mathlib3
feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`.
#2135
Merged
Merged
feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`. #2135
mergify
merged
27 commits into
master
from
add_monoid_algebra
pulling out convolution product
d2c3eebc
various
5a6377fd
chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin
0fae3fae
Merge branch 'is_noetherian_ring_fin_refactor' into add_monoid_algebra
5c638ffa
not there yet
15fe8bed
Merge branch 'is_noetherian_ring_fin_refactor' into is_integral_domai…
e0c9a490
feat(ring_theory/polynomial): refactor of is_integral_domain_fin
67cee3cd
fix
0646b4fa
Merge branch 'is_integral_domain_fin' into add_monoid_algebra
fa8109d7
..
d6af1336
refactor
43a61aee
fix
8afbcb0c
merge
20215285
yay
0324345a
cleanup
6ab2a296
merge
3c3fee40
satisfying the linter
f518dd3b
kim-em
commented
on 2020-03-12
kim-em
commented
on 2020-03-12
linter
f2cef76f
improving documentation
c4a3123d
jcommelin
commented
on 2020-03-12
jcommelin
commented
on 2020-03-12
add distrib instance for pointwise multiplication
f8653a08
merge
7538fa74
move files per Johan's suggestion
d44e2867
fix import
596486b6
jcommelin
commented
on 2020-03-19
Update src/data/polynomial.lean
1d379ed8
merge
f6f7f3bd
type annotation
a3d77392
jcommelin
approved these changes
on 2020-03-20
ChrisHughes24
approved these changes
on 2020-03-20
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into add_monoid_algebra
d04ca94a
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub