Commit 2020-09-16 08:03 4c9d3a58

View on Github →

feat(operator_norm): smul_right lemmas (#4150) from the sphere eversion project We need a version of continuous_linear_map.smul_right that is itself a continuous linear map from a normed space to a space of continuous linear maps. breaking changes:

rename smul_right_norm to norm_smul_right_apply
in homothety_norm remove useless sign assumption and switch from assuming positive dimension to nontrivial

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added def continuous_linear_map.apply

added def continuous_linear_map.applyₗ

added theorem continuous_linear_map.continuous_applyₗ

modified theorem continuous_linear_map.homothety_norm

added theorem continuous_linear_map.norm_smul_rightL

added theorem continuous_linear_map.norm_smul_rightL_apply

added theorem continuous_linear_map.norm_smul_right_apply

added def continuous_linear_map.smul_rightL

deleted theorem continuous_linear_map.smul_right_norm

Modified src/linear_algebra/basic.lean

added theorem submodule.nontrivial_span_singleton

Modified src/topology/algebra/module.lean

added def continuous_linear_map.smul_rightₗ