Theorem IsCyclotomicExtension.isAbelianGalois

Modification history

2025-10-18 16:44

Mathlib/NumberTheory/Cyclotomic/Basic.lean

feat(FieldTheory): abelian extensions (#23669)

Added IsCyclotomicExtension.isAbelianGalois View on Github →