Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 16:35 b7e20ca0

View on Github →

feat(data/polynomial/degree/definitions): two more nat_degree_le lemmas (#14098) This PR is similar to #14095. It proves the le version of nat_degree_X_pow and nat_degree_monomial. These lemmas are analogous to the existing nat_degree_X_le and nat_degree_C_mul_X_pow_le.

Estimated changes