Commit 2025-04-28 15:18 812fedbe

View on Github →

feat(Algebra/Polynomial): add lemmas (#23252)

Estimated changes

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

added theorem Polynomial.natDegree_finset_prod_X_sub_C_eq_card

Modified Mathlib/Algebra/Polynomial/Lifts.lean

added theorem Polynomial.monic_of_monic_mapAlg

Modified Mathlib/Algebra/Polynomial/Monic.lean

added theorem Polynomial.monic_finprod_of_monic

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added theorem Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero

Modified Mathlib/Algebra/Polynomial/Roots.lean

added theorem Polynomial.monic_finprod_X_sub_C

added theorem Polynomial.monic_multisetProd_X_sub_C

added theorem Polynomial.monic_prod_X_sub_C

deleted theorem Polynomial.monic_prod_multiset_X_sub_C

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C