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
.