Commit 2026-10-29 16:29 2556b1c7

View on Github →

chore(FieldTheory/KummerPolynomial): rename theorems (#45461) Rename theorems from X_pow_sub_C_irreducible to irreducible_X_pow_sub_C.

Estimated changes

Modified Mathlib/FieldTheory/KummerExtension.lean

deleted theorem X_pow_mul_sub_C_irreducible

deleted theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd

deleted theorem X_pow_sub_C_irreducible_iff_of_odd

deleted theorem X_pow_sub_C_irreducible_iff_of_prime_pow_of_ne_two

deleted theorem X_pow_sub_C_irreducible_of_odd

deleted theorem X_pow_sub_C_irreducible_of_prime_pow_of_ne_two

added theorem irreducible_X_pow_mul_sub_C

added theorem irreducible_X_pow_sub_C_iff_forall_prime_of_odd

added theorem irreducible_X_pow_sub_C_iff_of_odd

added theorem irreducible_X_pow_sub_C_iff_of_prime_pow_of_ne_two

added theorem irreducible_X_pow_sub_C_of_odd

added theorem irreducible_X_pow_sub_C_of_prime_pow_of_ne_two

Modified Mathlib/FieldTheory/KummerPolynomial.lean

deleted theorem X_pow_sub_C_irreducible_iff_of_prime

deleted theorem X_pow_sub_C_irreducible_of_prime

added theorem irreducible_X_pow_sub_C_iff_of_prime

added theorem irreducible_X_pow_sub_C_of_prime

Modified Mathlib/FieldTheory/Perfect.lean