Commit 2025-06-23 14:57 f0f62b72

View on Github →

feat(NumberTheory/Cyclotomic/Basic): generalize some results for cyclotomic field (#26266)

  • generalize IsCyclotomicExtension.neZero['] to IsCyclotomicExtension.neZero_of_mem['] which states that any non-zero element in S is non-zero in the ring
  • generalize IsCyclotomicExtension.integral to any ring, without Noetherian and finiteness of S
  • 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 to IsSepClosed
  • add a missing instance SeparableClosure.isSepClosed
  • add some more instances for HasEnoughRootsOfUnity

Estimated changes