cont_diff): generalize `mul` lemmas to a normed algebra (#15595)

Commit

3 years ago

feat(analysis/calculus/cont_diff): generalize `mul` lemmas to a normed algebra (#15595) Also add lemmas about `finset.prod`.

Author

urkud

Parents