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

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