Commit 2024-10-22 13:55 ac12c873

View on Github →

chore(Algebra/Polynomial/RingDivision): move lemmas earlier (#18050) Algebra.Polynomial.RingDivision is a bag grab of lemmas with absolutely no running theme. This PR moves two thirds of them to earlier files with no proof change.

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.X_sub_C_pow_dvd_iff

modified theorem Polynomial.aeval_endomorphism

added theorem Polynomial.comp_X_add_C_eq_zero_iff

added theorem Polynomial.comp_X_add_C_ne_zero_iff

added theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul

added theorem Polynomial.nmem_nonZeroDivisors_iff

added theorem Polynomial.units_coeff_zero_smul

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

added theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card

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

added theorem Polynomial.Monic.C_dvd_iff_isUnit

added theorem Polynomial.Monic.degree_pos

added theorem Polynomial.Monic.degree_pos_of_not_isUnit

added theorem Polynomial.Monic.natDegree_pos

added theorem Polynomial.Monic.natDegree_pos_of_not_isUnit

added theorem Polynomial.coeff_coe_units_zero_ne_zero

added theorem Polynomial.degree_coe_units

added theorem Polynomial.degree_eq_zero_of_isUnit

added theorem Polynomial.degree_le_mul_left

added theorem Polynomial.degree_le_of_dvd

modified theorem Polynomial.degree_mul

added theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic

modified theorem Polynomial.degree_pow

added theorem Polynomial.eq_zero_of_dvd_of_degree_lt

added theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt

added theorem Polynomial.isUnit_iff

modified theorem Polynomial.leadingCoeffHom_apply

modified theorem Polynomial.leadingCoeff_dvd_leadingCoeff

modified theorem Polynomial.leadingCoeff_mul

modified theorem Polynomial.leadingCoeff_pow

added theorem Polynomial.natDegree_coe_units

added theorem Polynomial.natDegree_eq_zero_of_isUnit

added theorem Polynomial.natDegree_le_of_dvd

added theorem Polynomial.natDegree_mul

added theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic

added theorem Polynomial.natDegree_pow

added theorem Polynomial.natDegree_sub_eq_of_prod_eq

added theorem Polynomial.not_dvd_of_degree_lt

added theorem Polynomial.not_dvd_of_natDegree_lt

added theorem Polynomial.not_isUnit_of_degree_pos

added theorem Polynomial.not_isUnit_of_natDegree_pos

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

added theorem Polynomial.comp_eq_zero_iff

added theorem Polynomial.comp_neg_X_leadingCoeff_eq

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Polynomial.add_modByMonic

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.degree_eq_one_of_irreducible_of_root

added theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le

added theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff

added theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le

added theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp

added theorem Polynomial.le_rootMultiplicity_iff

added theorem Polynomial.le_rootMultiplicity_mul

added theorem Polynomial.leadingCoeff_divByMonic_X_sub_C

added theorem Polynomial.leadingCoeff_divByMonic_of_monic

added theorem Polynomial.modByMonic_eq_of_dvd_sub

added theorem Polynomial.neg_modByMonic

added theorem Polynomial.pow_rootMultiplicity_not_dvd

added theorem Polynomial.rootMultiplicity_add

added theorem Polynomial.rootMultiplicity_eq_natTrailingDegree'

added theorem Polynomial.rootMultiplicity_le_iff

added theorem Polynomial.sub_modByMonic

Modified Mathlib/Algebra/Polynomial/Eval.lean

added theorem Polynomial.Monic.irreducible_of_irreducible_map

added theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map

added theorem Polynomial.root_mul

added theorem Polynomial.root_or_root_of_root_mul

Modified Mathlib/Algebra/Polynomial/Mirror.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

added theorem Polynomial.Monic.comp

added theorem Polynomial.Monic.comp_X_add_C

added theorem Polynomial.Monic.comp_X_sub_C

added theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt

added theorem Polynomial.Monic.irreducible_iff_natDegree'

added theorem Polynomial.Monic.irreducible_iff_natDegree

added theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff

added theorem Polynomial.irreducible_of_monic

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

deleted theorem Polynomial.Monic.C_dvd_iff_isUnit

deleted theorem Polynomial.Monic.comp

deleted theorem Polynomial.Monic.comp_X_add_C

deleted theorem Polynomial.Monic.comp_X_sub_C

deleted theorem Polynomial.Monic.degree_pos

deleted theorem Polynomial.Monic.degree_pos_of_not_isUnit

deleted theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt

deleted theorem Polynomial.Monic.irreducible_iff_natDegree'

deleted theorem Polynomial.Monic.irreducible_iff_natDegree

deleted theorem Polynomial.Monic.irreducible_of_irreducible_map

deleted theorem Polynomial.Monic.natDegree_pos

deleted theorem Polynomial.Monic.natDegree_pos_of_not_isUnit

deleted theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff

deleted theorem Polynomial.X_sub_C_pow_dvd_iff

deleted theorem Polynomial.add_modByMonic

deleted theorem Polynomial.associated_of_dvd_of_degree_eq

deleted theorem Polynomial.associated_of_dvd_of_natDegree_le

deleted theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff

deleted theorem Polynomial.coeff_coe_units_zero_ne_zero

deleted theorem Polynomial.comp_X_add_C_eq_zero_iff

deleted theorem Polynomial.comp_X_add_C_ne_zero_iff

deleted theorem Polynomial.comp_eq_zero_iff

deleted theorem Polynomial.comp_neg_X_leadingCoeff_eq

deleted theorem Polynomial.degree_coe_units

deleted theorem Polynomial.degree_eq_one_of_irreducible_of_root

deleted theorem Polynomial.degree_eq_zero_of_isUnit

deleted theorem Polynomial.degree_le_mul_left

deleted theorem Polynomial.degree_le_of_dvd

deleted theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic

deleted theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le

deleted theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff

deleted theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le

deleted theorem Polynomial.eq_zero_of_dvd_of_degree_lt

deleted theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt

deleted theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul

deleted theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp

deleted theorem Polynomial.irreducible_of_monic

deleted theorem Polynomial.isUnit_iff

deleted theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map

deleted theorem Polynomial.le_rootMultiplicity_iff

deleted theorem Polynomial.le_rootMultiplicity_mul

deleted theorem Polynomial.leadingCoeff_divByMonic_X_sub_C

deleted theorem Polynomial.leadingCoeff_divByMonic_of_monic

deleted theorem Polynomial.modByMonic_eq_of_dvd_sub

deleted theorem Polynomial.natDegree_coe_units

deleted theorem Polynomial.natDegree_eq_zero_of_isUnit

deleted theorem Polynomial.natDegree_le_of_dvd

deleted theorem Polynomial.natDegree_mul

deleted theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card

deleted theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic

deleted theorem Polynomial.natDegree_pow

deleted theorem Polynomial.natDegree_sub_eq_of_prod_eq

deleted theorem Polynomial.neg_modByMonic

deleted theorem Polynomial.nmem_nonZeroDivisors_iff

deleted theorem Polynomial.not_dvd_of_degree_lt

deleted theorem Polynomial.not_dvd_of_natDegree_lt

deleted theorem Polynomial.not_isUnit_of_degree_pos

deleted theorem Polynomial.not_isUnit_of_natDegree_pos

deleted theorem Polynomial.pow_rootMultiplicity_not_dvd

deleted theorem Polynomial.rootMultiplicity_add

deleted theorem Polynomial.rootMultiplicity_eq_natTrailingDegree'

deleted theorem Polynomial.rootMultiplicity_le_iff

deleted theorem Polynomial.root_mul

deleted theorem Polynomial.root_or_root_of_root_mul

deleted theorem Polynomial.sub_modByMonic

deleted theorem Polynomial.units_coeff_zero_smul

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/FieldTheory/RatFunc/Defs.lean

Modified Mathlib/RingTheory/Polynomial/IrreducibleRing.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified scripts/no_lints_prime_decls.txt