Commit 2023-01-03 11:06 44b58b42

View on Github →

feat(topology/algebra/module/multilinear): add continuous versions of constructions (#18044) One of these is a much more general case of continuous_multilinear_map.curry0; but to keep this PR small we don't attempt to remove curry0, instead just golfing it.

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.nnnorm_const_of_is_empty

added theorem continuous_multilinear_map.nnnorm_of_subsingleton

added theorem continuous_multilinear_map.norm_const_of_is_empty

added theorem continuous_multilinear_map.norm_of_subsingleton

Modified src/linear_algebra/alternating.lean

Modified src/linear_algebra/multilinear/basic.lean

Modified src/linear_algebra/pi_tensor_product.lean

Modified src/topology/algebra/module/multilinear.lean

added def continuous_multilinear_map.const_of_is_empty

added def continuous_multilinear_map.of_subsingleton