Commit 2025-06-23 14:57 f0f62b72
View on Github →feat(NumberTheory/Cyclotomic/Basic): generalize some results for cyclotomic field (#26266)
- generalize
IsCyclotomicExtension.neZero[']
toIsCyclotomicExtension.neZero_of_mem[']
which states that any non-zero element inS
is non-zero in the ring - generalize
IsCyclotomicExtension.integral
to any ring, without Noetherian and finiteness ofS
- add
IsCyclotomicExtension.isSeparable
that any cyclotomic extension is separable - add
IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_(isSepClosed|exists_isPrimitiveRoot)
that any cyclotomic extension is isomorphic to a field extension adjoin roots of unity - add
(Algebra|IntermediateField).isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot
that an algebra or field extension adjoin roots of unity is cyclotomic - generalize
IsCyclotomicExtension.isGalois
to any cyclotomic extension - generalize
IsCyclotomicExtension.algEquiv
to any cyclotomic extension - remove duplicated instance
CyclotomicField.algebra'
(was different in mathlib3, but becomes the same in mathlib4) - generalize some results from
IsAlgClosed
toIsSepClosed
- add a missing instance
SeparableClosure.isSepClosed
- add some more instances for
HasEnoughRootsOfUnity