Notation for Galois group

The Galois group Gal(L/K) is implemented via L ≃ₐ[K] L in mathlib. We provide such a notation in this file.

Although this notation works for all automorphism groups of algebras, we should only use this notation when L/K is an extension of fields.

def «termGal(_/_)» : Lean.ParserDescr

Notation for Gal(L/K) := L ≃ₐ[K] L.

L ≃ₐ[K] L will pretty-print as Gal(L/K) when L and K are both fields.

Although this notation works for all automorphism groups of algebras, we should only use this notation when L/K is an extension of fields.

Equations

• One or more equations did not get rendered due to their size.

def delabGal : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer for the Gal(L/K) notation.

Equations

• One or more equations did not get rendered due to their size.