Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-07 04:25 ebe2c616

View on Github →

feat(analysis/normed_space/multilinear): a few more bundled (bi)linear maps (#6546)

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

added def continuous_linear_map.comp_continuous_multilinear_mapL

added def continuous_linear_map.flip_multilinear

modified theorem continuous_linear_map.norm_comp_continuous_multilinear_map_le

added def continuous_multilinear_map.comp_continuous_linear_mapL

added theorem continuous_multilinear_map.comp_continuous_linear_mapL_apply

added theorem continuous_multilinear_map.norm_comp_continuous_linear_le

added theorem continuous_multilinear_map.norm_comp_continuous_linear_mapL_le

modified theorem continuous_multilinear_map.norm_mk_pi_algebra_fin

added theorem continuous_multilinear_map.op_norm_prod

added def continuous_multilinear_map.prodL