Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-11 12:23 e0093544

View on Github →

chore(data/mv_polynomials): golf, add a lemma (#9132)

  • add monoid_algebra.support_mul_single;
  • transfer a few more lemmas from monoid_algebra to add_monoid_algebra
  • add mv_polynomial.support_mul_X
  • reuse a proof.

Estimated changes