definition): nat_degree_monomial in ite form (#11123)

Commit

4 years ago

feat(data/polynomial/degree/definition): nat_degree_monomial in ite form (#11123) Changed the proof usage elsewhere. This helps deal with sums of over monomials.

Author

pechersky

Parents

424773a7

mathlib3 ac976755 - feat(data/polynomial/degree/definition): nat_degree_monomial in ite form (#11123)

mathlib3
ac976755 - feat(data/polynomial/degree/definition): nat_degree_monomial in ite form (#11123)