mathlib

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

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 `namespace`s.