Commit 2025-01-14 06:06 c083085d

View on Github →

refactor(FieldTheory/KummerExtension): Split off irreducibility of X ^ p - a (#20695) This PR splits of irreducibility of X ^ p - a from FieldTheory/KummerExtension since it has lighter imports and can be used to golf a proof in FieldTheory/Perfect.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

deleted theorem X_pow_sub_C_irreducible_iff_of_prime

deleted theorem X_pow_sub_C_irreducible_of_prime

deleted theorem ne_zero_of_irreducible_X_pow_sub_C'

deleted theorem ne_zero_of_irreducible_X_pow_sub_C

deleted theorem pow_ne_of_irreducible_X_pow_sub_C

deleted theorem root_X_pow_sub_C_eq_zero_iff

deleted theorem root_X_pow_sub_C_ne_zero'

deleted theorem root_X_pow_sub_C_ne_zero

deleted theorem root_X_pow_sub_C_ne_zero_iff

deleted theorem root_X_pow_sub_C_pow

Created Mathlib/FieldTheory/KummerPolynomial.lean

added theorem X_pow_sub_C_irreducible_iff_of_prime

added theorem X_pow_sub_C_irreducible_of_prime

added theorem ne_zero_of_irreducible_X_pow_sub_C'

added theorem ne_zero_of_irreducible_X_pow_sub_C

added theorem pow_ne_of_irreducible_X_pow_sub_C

added theorem root_X_pow_sub_C_eq_zero_iff

added theorem root_X_pow_sub_C_ne_zero'

added theorem root_X_pow_sub_C_ne_zero

added theorem root_X_pow_sub_C_ne_zero_iff

added theorem root_X_pow_sub_C_pow

Modified Mathlib/FieldTheory/Perfect.lean