Commit 2025-05-31 11:37 bc40dcfb

View on Github →

chore(CyclotomicField): use Nat instead of PNat (#25114) See Zulip

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

modified theorem IsAlgClosed.isCyclotomicExtension

modified theorem IsCyclotomicExtension.adjoin_primitive_root_eq_top

modified theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots

modified theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic

added theorem IsCyclotomicExtension.eq_self_sdiff_zero

modified theorem IsCyclotomicExtension.exists_prim_root

modified theorem IsCyclotomicExtension.iff_union_of_dvd

modified theorem IsCyclotomicExtension.isSplittingField_X_pow_sub_one

modified theorem IsCyclotomicExtension.neZero'

modified theorem IsCyclotomicExtension.neZero

modified theorem IsCyclotomicExtension.of_union_of_dvd

modified theorem IsCyclotomicExtension.subsingleton_iff

modified theorem IsPrimitiveRoot.adjoin_isCyclotomicExtension

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

modified theorem IsCyclotomicExtension.discr_odd_prime

modified theorem IsCyclotomicExtension.discr_prime_pow

modified theorem IsCyclotomicExtension.discr_prime_pow_ne_two'

modified theorem IsCyclotomicExtension.discr_prime_pow_ne_two

Modified Mathlib/NumberTheory/Cyclotomic/Embeddings.lean

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/NumberTheory/Cyclotomic/PID.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

modified theorem IsCyclotomicExtension.aeval_zeta

modified theorem IsCyclotomicExtension.finrank

modified theorem IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two

modified theorem IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two

modified theorem IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow

modified theorem IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two

modified theorem IsCyclotomicExtension.zeta_isRoot

modified theorem IsCyclotomicExtension.zeta_pow

modified theorem IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero

modified theorem IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two

modified theorem IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two

modified theorem IsPrimitiveRoot.norm_sub_one_of_prime_ne_two'

modified theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic

modified theorem IsPrimitiveRoot.sub_one_norm_isPrimePow

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

modified theorem IsCyclotomicExtension.Rat.discr_prime_pow'

modified theorem IsPrimitiveRoot.card_quotient_toInteger_sub_one

modified theorem IsPrimitiveRoot.coe_toInteger

modified theorem IsPrimitiveRoot.finite_quotient_toInteger_sub_one

modified theorem IsPrimitiveRoot.toInteger_isPrimitiveRoot

modified theorem IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

Modified Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.lean