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.