Commit 2024-01-06 20:00 1b3fb343

View on Github →

feat: Criteria for X ^ n - C a to be irreducible for odd n. (#9397)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Power.lean

added theorem Commute.exists_eq_pow_of_pow_eq_pow_of_coprime

added theorem pow_mem_range_pow_of_coprime

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.associated_of_dvd_of_degree_eq

added theorem Polynomial.associated_of_dvd_of_natDegree_le

added theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff

added theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.AdjoinSimple.coe_gen

added theorem IntermediateField.adjoin_root_eq_top

added theorem IntermediateField.finrank_top'

added theorem IntermediateField.rank_top'

added theorem Polynomial.irreducible_comp

Modified Mathlib/FieldTheory/IntermediateField.lean

added theorem IntermediateField.algebraMap_apply

added theorem IntermediateField.coe_algebraMap_apply

Modified Mathlib/FieldTheory/KummerExtension.lean

added theorem X_pow_mul_sub_C_irreducible

added theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd

added theorem X_pow_sub_C_irreducible_iff_of_odd

added theorem X_pow_sub_C_irreducible_iff_of_prime

added theorem X_pow_sub_C_irreducible_iff_of_prime_pow

added theorem X_pow_sub_C_irreducible_of_odd

added theorem X_pow_sub_C_irreducible_of_prime

added theorem X_pow_sub_C_irreducible_of_prime_pow

added theorem pow_ne_of_irreducible_X_pow_sub_C