Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

Modified src/data/finsupp.lean

deleted theorem finsupp.mul_def

deleted theorem finsupp.one_def

deleted theorem finsupp.prod_single

deleted theorem finsupp.single_mul_single

deleted theorem finsupp.support_mul

Created src/data/finsupp/pointwise.lean

added theorem finsupp.mul_apply

added theorem finsupp.support_mul

Created src/data/monoid_algebra.lean

added theorem add_monoid_algebra.mul_def

added theorem add_monoid_algebra.one_def

added theorem add_monoid_algebra.prod_single

added theorem add_monoid_algebra.single_mul_single

added theorem add_monoid_algebra.support_mul

added def add_monoid_algebra

added theorem monoid_algebra.mul_def

added theorem monoid_algebra.one_def

added theorem monoid_algebra.prod_single

added theorem monoid_algebra.single_mul_single

added theorem monoid_algebra.support_mul

added def monoid_algebra

Modified src/data/mv_polynomial.lean

added def mv_polynomial.coeff_coe_to_fun

modified def mv_polynomial

Modified src/data/polynomial.lean

modified def polynomial.C

modified def polynomial.X

added def polynomial.monomial

modified theorem polynomial.single_eq_C_mul_X

modified def polynomial

Modified src/linear_algebra/finsupp.lean

Modified src/ring_theory/polynomial.lean

Modified src/ring_theory/power_series.lean

deleted def polynomial.monomial