Commit 2025-10-18 16:44 06ed561e

View on Github →

feat(FieldTheory): abelian extensions (#23669)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Galois/Abelian.lean

added theorem IsAbelianGalois.of_algHom

added theorem IsAbelianGalois.of_isCyclic

added theorem IsAbelianGalois.tower_bot

added theorem IsAbelianGalois.tower_top

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

added theorem IsCyclotomicExtension.isAbelianGalois