basic): `pi` and `prod` are `normed_algebra`s (#13442)

Commit

3 years ago

feat(analysis/normed_space/basic): `pi` and `prod` are `normed_algebra`s (#13442) Note that over an empty index type, `pi` is not a normed_algebra since it is trivial as a ring.

Author

eric-wieser

Parents

d13f291b

mathlib ebc8b441 - feat(analysis/normed_space/basic): `pi` and `prod` are `normed_algebra`s (#13442)

mathlib
ebc8b441 - feat(analysis/normed_space/basic): `pi` and `prod` are `normed_algebra`s (#13442)