Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 16:06 76ab749e

View on Github →

feat(analysis/normed_space/operator_norm): variants of continuous_linear_map.lsmul and their properties (#8984)

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.norm_to_span_singleton

added theorem continuous_linear_map.to_span_singleton_add

added theorem continuous_linear_map.to_span_singleton_apply

added theorem continuous_linear_map.to_span_singleton_smul'

added theorem continuous_linear_map.to_span_singleton_smul