Commit 2021-02-08 21:41 7f11d721
View on Github →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ₗ
andcontinuous_linear_map.prodₗᵢ
; - add
prod.topological_semimodule
; - drop unused
is_bounded_linear_map_prod_iso
.