mathlib

46b0528b - refactor(data/polynomial): Move some lemmas to `monoid_algebra` (#4627)

refactor(data/polynomial): Move some lemmas to `monoid_algebra` (#4627) The `add_monoid_algebra.mul_apply_antidiagonal` lemma is copied verbatim from `monoid_algebra.mul_apply_antidiagonal`.