mathlib3
feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`.
#2135
Merged
Overview
Commits
27
Changes
View On GitHub
Commits
  • pulling out convolution product
    kim-em committed 6 years ago
  • various
    kim-em committed 6 years ago
  • chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin
    kim-em committed 6 years ago
  • Merge branch 'is_noetherian_ring_fin_refactor' into add_monoid_algebra
    kim-em committed 6 years ago
  • not there yet
    kim-em committed 6 years ago
  • Merge branch 'is_noetherian_ring_fin_refactor' into is_integral_domain_fin
    kim-em committed 6 years ago
  • feat(ring_theory/polynomial): refactor of is_integral_domain_fin
    kim-em committed 6 years ago
  • fix
    kim-em committed 6 years ago
  • Merge branch 'is_integral_domain_fin' into add_monoid_algebra
    kim-em committed 6 years ago
  • ..
    kim-em committed 6 years ago
  • refactor
    kim-em committed 6 years ago
  • fix
    kim-em committed 6 years ago
  • merge
    kim-em committed 6 years ago
  • yay
    kim-em committed 6 years ago
  • cleanup
    kim-em committed 6 years ago
  • merge
    kim-em committed 6 years ago
  • satisfying the linter
    kim-em committed 6 years ago
  • linter
    kim-em committed 6 years ago
  • improving documentation
    kim-em committed 6 years ago
  • add distrib instance for pointwise multiplication
    kim-em committed 6 years ago
  • merge
    kim-em committed 6 years ago
  • move files per Johan's suggestion
    kim-em committed 6 years ago
  • fix import
    kim-em committed 6 years ago
  • Update src/data/polynomial.lean
    kim-em committed 6 years ago
  • merge
    kim-em committed 6 years ago
  • type annotation
    kim-em committed 6 years ago
  • Merge branch 'master' into add_monoid_algebra
    mergify[bot] committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading