definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095)

Commit

3 years ago

feat(data/polynomial/degree/definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095) Add a lemma analogous to `nat_degree_C_mul_X_pow` and `nat_degree_C_mul_X`.

Author

adomani

Parents

59273305

mathlib c2e87de5 - feat(data/polynomial/degree/definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095)

mathlib
c2e87de5 - feat(data/polynomial/degree/definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095)