mathlib3

7ad184e3 - fix(data/polynomial/basic): remove `monomial_fun` to remove diamonds (#15778)

fix(data/polynomial/basic): remove `monomial_fun` to remove diamonds (#15778) This was previously irreducible to prevent any `finsupp/add_monoid_algebra` leakage, but it causes a non-defeq diamond in instances. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>