Commit 2024-09-06 01:15 1c51e108

View on Github →

feat(Algebra/Polynomial/Basic): miscellaneous basic lemmas on polynomials (#16372)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.X_ne_C

added theorem Polynomial.coeff_monomial_of_ne

added theorem Polynomial.coeff_monomial_same

added theorem Polynomial.monomial_eq_monomial_iff

Modified Mathlib/Algebra/Polynomial/Lifts.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

added theorem Polynomial.coeffs_monomial