Commit 2026-10-17 10:25 58f2f217

View on Github →

refactor: move results about polynomial degrees outside of the FiniteField namespace (#44691) They don't depend on the polynomial being over a finite field, at all.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/Operations.lean

added theorem FiniteField.X_pow_card_pow_sub_X_natDegree_eq

added theorem FiniteField.X_pow_card_pow_sub_X_ne_zero

added theorem Polynomial.X_pow_sub_X_ne_zero

modified theorem Polynomial.degree_X_pow_sub_C

added theorem Polynomial.degree_X_pow_sub_X

modified theorem Polynomial.natDegree_X_pow_sub_C

added theorem Polynomial.natDegree_X_pow_sub_X

Modified Mathlib/FieldTheory/Finite/Basic.lean

deleted theorem FiniteField.X_pow_card_pow_sub_X_natDegree_eq

deleted theorem FiniteField.X_pow_card_pow_sub_X_ne_zero

deleted theorem FiniteField.X_pow_card_sub_X_natDegree_eq

deleted theorem FiniteField.X_pow_card_sub_X_ne_zero

Modified Mathlib/FieldTheory/Finite/Extension.lean

modified theorem Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Galois/NormalBasis.lean

Modified Mathlib/FieldTheory/KummerPolynomial.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean