Commit 2025-11-05 17:11 e2a1cd1d

View on Github →

feat(Algebra/Polynomial): small and useful lemmas (#29956)

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

modified theorem Polynomial.isRoot_of_aeval_algebraMap_eq_zero

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.C_ofNat

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

added theorem Polynomial.degree_map_eq_of_injective

added theorem Polynomial.degree_map_eq_of_isUnit_leadingCoeff

added theorem Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff

added theorem Polynomial.leadingCoeff_map_of_injective

added theorem Polynomial.natDegree_map_eq_of_injective

added theorem Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff

added theorem Polynomial.nextCoeff_C_mul

added theorem Polynomial.nextCoeff_map

added theorem Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff

added theorem Polynomial.nextCoeff_mul_C

added theorem Polynomial.subsingleton_isRoot_of_natDegree_eq_one

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Irreducible.isRoot_eq_bot_of_natDegree_ne_one

added theorem Irreducible.not_isRoot_of_natDegree_ne_one

added theorem Irreducible.subsingleton_isRoot

added theorem Polynomial.rootMultiplicity_le_rootMultiplicity_of_dvd

Modified Mathlib/Algebra/Polynomial/Eval/Coeff.lean

added theorem Polynomial.zero_isRoot_iff_coeff_zero_eq_zero

deleted theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

added theorem Polynomial.eval_map_apply

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

added theorem Polynomial.nextCoeff_map_of_leadingCoeff_ne_zero

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

modified theorem Polynomial.degree_map

modified theorem Polynomial.leadingCoeff_map

modified theorem Polynomial.map_ne_zero

modified theorem Polynomial.monic_map_iff

modified theorem Polynomial.natDegree_map

added theorem Polynomial.nextCoeff_map_eq

Modified Mathlib/Algebra/Polynomial/Monic.lean

modified theorem Polynomial.Monic.map

deleted theorem Polynomial.degree_map_eq_of_injective

deleted theorem Polynomial.leadingCoeff_map_of_injective

deleted theorem Polynomial.natDegree_map_eq_of_injective

deleted theorem Polynomial.nextCoeff_map

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added theorem Irreducible.aeval_ne_zero_of_natDegree_ne_one

Modified Mathlib/Algebra/Polynomial/Roots.lean

added theorem Associated.roots_eq

modified theorem Polynomial.Monic.irreducible_iff_degree_lt

added theorem Polynomial.card_roots_le_one_of_irreducible

added theorem Polynomial.card_roots_map_le_degree

added theorem Polynomial.card_roots_map_le_natDegree

added theorem Polynomial.filter_roots_map_range_eq_map_roots

added theorem Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot

added theorem Polynomial.roots_eq_zero_iff_isRoot_eq_bot

added theorem Polynomial.roots_eq_zero_of_irreducible_of_natDegree_ne_one

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits

added theorem Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.associated_iff_roots_eq_roots

added theorem IsAlgClosed.card_aroots_eq_natDegree

added theorem IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff

added theorem IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero

added theorem IsAlgClosed.card_roots_eq_natDegree

added theorem IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing

added theorem IsAlgClosed.card_roots_map_eq_natDegree_of_injective

added theorem IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff

added theorem IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero

added theorem IsAlgClosed.dvd_iff_roots_le_roots

modified theorem IsAlgClosed.exists_aeval_eq_zero

modified theorem IsAlgClosed.exists_eval₂_eq_zero

added theorem IsAlgClosed.roots_eq_zero_iff_degree_nonpos

added theorem IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero

Modified Mathlib/FieldTheory/IsSepClosed.lean

modified theorem IsSepClosed.exists_aeval_eq_zero

modified theorem IsSepClosed.exists_eval₂_eq_zero

added theorem IsSepClosed.exists_eval₂_eq_zero_of_injective

Modified Mathlib/FieldTheory/NormalizedTrace.lean

Modified Mathlib/RingTheory/Trace/Basic.lean