Mathlib Changelog
v3
Changelog
About
Github
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