Commit 2021-05-14 19:19 fd3d1178

View on Github →

feat(data/mv_polynomial/basic): Add ring section (#7507) A few lemmas about monomial analogous to those for the single-variate polynomials over rings.

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.single_nat_sub

added theorem finsupp.single_neg

modified theorem finsupp.single_sub

Modified src/data/mv_polynomial/basic.lean

Modified src/data/mv_polynomial/comm_ring.lean

added theorem mv_polynomial.monomial_neg

added theorem mv_polynomial.monomial_sub