Mathlib v3 is deprecated. Go to Mathlib v4

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ₗ and continuous_linear_map.prodₗᵢ;
  • add prod.topological_semimodule;
  • drop unused is_bounded_linear_map_prod_iso.

Estimated changes