Commit 2021-12-13 07:52 214a80f3

View on Github →

feat(data/mv_polynomial/variables): API for mv_polynomial.degree_of (#10646) This PR provides some API for mv_polynomial.degree_of for comm_ring and comm_semiring. I don't know which of these lemmas should be simp lemmas.

Estimated changes

Modified src/data/finset/lattice.lean

added theorem multiset.count_finset_sup

deleted theorem multiset.count_sup

Modified src/data/finsupp/basic.lean

modified theorem finsupp.support_neg

added theorem finsupp.support_sub

Modified src/data/mv_polynomial/comm_ring.lean

added theorem mv_polynomial.degree_of_sub_lt

added theorem mv_polynomial.support_sub

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.degree_of_C

added theorem mv_polynomial.degree_of_X

added theorem mv_polynomial.degree_of_add_le

added theorem mv_polynomial.degree_of_eq_sup

added theorem mv_polynomial.degree_of_lt_iff

added theorem mv_polynomial.degree_of_mul_X_eq

added theorem mv_polynomial.degree_of_mul_X_ne

added theorem mv_polynomial.degree_of_mul_le

added theorem mv_polynomial.monomial_le_degree_of

Modified src/ring_theory/mv_polynomial/basic.lean