mathlib

7f11d721 - feat(analysis/normed_space): `continuous_linear_map.prod` as a `linear_isometry_equiv` (#6099)

feat(analysis/normed_space): `continuous_linear_map.prod` as a `linear_isometry_equiv` (#6099) * add lemma `continuous_linear_map.op_norm_prod`; * add `continuous_linear_map.prodₗ` and `continuous_linear_map.prodₗᵢ`; * add `prod.topological_semimodule`; * drop unused `is_bounded_linear_map_prod_iso`. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>