Commit 2025-11-26 16:01 5c71dcf6

View on Github →

feat(CyclotomicFields): generalize IsPrimitiveRoot.integralPowerBasis to all (nonzero) integers (#30010)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

added theorem IsCyclotomicExtension.Rat.adjoin_singleton_eq_top

added theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure

modified theorem IsCyclotomicExtension.Rat.discr

added theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton

added theorem IsCyclotomicExtension.Rat.natAbs_discr

deleted theorem IsPrimitiveRoot.integralPowerBasis'_gen

added theorem IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim

added theorem IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen

modified theorem IsPrimitiveRoot.integralPowerBasis_dim

modified theorem IsPrimitiveRoot.integralPowerBasis_gen

deleted theorem IsPrimitiveRoot.power_basis_int'_dim

deleted theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen

deleted theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime

added theorem IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen

added theorem IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime

modified theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen

deleted theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime