Commit 2025-10-16 07:33 ed5b08ca

View on Github →

feat: notation for galois group (#30266) This PR adds support for the notation Gal(L/K) := L ≃ₐ[K] L. Gal(L/K) is a simple macro for L ≃ₐ[K] L, but L ≃ₐ[K] L only delaborates to Gal(L/K) when L and K are fields. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Notation.20for.20Galois.20group/with/543320864

Estimated changes

modified theorem spectralNorm_eq_of_equiv
modified theorem IsGalois.map_fixingSubgroup
modified theorem IsGalois.normalBasis_apply
modified def fixedByFinite
modified def galBasis
modified theorem mem_galBasis_iff
modified theorem autEquivRootsOfUnity_smul
modified def Normal.algHomEquivAut
modified theorem coe_galRestrict_apply
modified def galRestrict
modified theorem galRestrict_apply