Skip to content

Commit

Permalink
doc(data/finsupp/pointwise): update old module doc (#7770)
Browse files Browse the repository at this point in the history


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Jun 2, 2021
1 parent b91cdb9 commit b231c92
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/data/finsupp/pointwise.lean
Expand Up @@ -8,10 +8,10 @@ import data.finsupp.basic
/-!
# The pointwise product on `finsupp`.
TODO per issue #1864:
We intend to remove the convolution product on finsupp, and define
it only on a type synonym `add_monoid_algebra`. After we've done this,
it would be good to make this the default product on `finsupp`.
For the convolution product on `finsupp` when the domain has a binary operation,
see the type synonyms `add_monoid_algebra`
(which is in turn used to define `polynomial` and `mv_polynomial`)
and `monoid_algebra`.
-/

noncomputable theory
Expand Down

0 comments on commit b231c92

Please sign in to comment.