Commit 2020-03-20 17:26 8d44098d
View on Github →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