Commit 2023-08-02 03:48 8fd5c885

View on Github →

chore: golf Polynomial.degree_mul_le (#6263) And other similar lemmas With thanks to @adomani for adding these lemmas.

Estimated changes

Modified Mathlib/Data/MvPolynomial/Variables.lean

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.support_toFinsupp

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

modified theorem Polynomial.degree_add_le

modified theorem Polynomial.degree_mul_le