Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-04 03:36 aa1dbeab

View on Github →

chore(analysis/normed_space/extend): golf, add aux lemmas (#18927)

Add linear_map.extend_to_𝕜'_apply_re, linear_map.sq_norm_extend_to_𝕜'_apply, continuous_linear_map.norm_extend_to_𝕜, and continuous_linear_map.norm_extend_to_𝕜'.
Rename norm_bound to continuous_linear_map.norm_extend_to_𝕜'_bound.
Golf, use namespaces.

Estimated changes

Modified src/analysis/normed_space/extend.lean

modified theorem continuous_linear_map.extend_to_𝕜'_apply

added theorem continuous_linear_map.norm_extend_to_𝕜'

added theorem continuous_linear_map.norm_extend_to_𝕜'_bound

added theorem continuous_linear_map.norm_extend_to_𝕜

modified theorem linear_map.extend_to_𝕜'_apply

added theorem linear_map.extend_to_𝕜'_apply_re

added theorem linear_map.norm_extend_to_𝕜'_apply_sq

deleted theorem norm_bound

Modified src/analysis/normed_space/hahn_banach/extension.lean