mathlib3
65335003 - feat(data/mv_polynomial): add total_degree_add_of_total_degree_lt (#10571)

Commit

4 years ago

feat(data/mv_polynomial): add total_degree_add_of_total_degree_lt (#10571) A helpful lemma to compute total degrees from flt-regular.

Author

alexjbest

Parents