mathlib

8d44098d - feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`. (#2135)

feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`. (#2135) * pulling out convolution product * various * chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin * not there yet * feat(ring_theory/polynomial): refactor of is_integral_domain_fin * fix * .. * refactor * fix * yay * cleanup * satisfying the linter * linter * improving documentation * add distrib instance for pointwise multiplication * move files per Johan's suggestion * fix import * Update src/data/polynomial.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * type annotation Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>