feat(analysis/normed_space/operator_norm): remove to_span_singleton_n…

…orm (#16654) Remove `continuous_linear_map.to_span_singleton_norm`. It is a duplicate of `continuous_linear_map.norm_to_span_singleton` (which has more explicit arguments and weaker type-class assumptions).
leanprover-community · Sep 27, 2022 · e46daa0 · e46daa0
1 parent 1a4f927
commit e46daa0
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
@@ -1258,9 +1258,6 @@ begin
   simpa only [hf, hx, mul_le_mul_right] using f.le_op_norm x,
 end
 
-lemma to_span_singleton_norm (x : E) : ∥to_span_singleton 𝕜 x∥ = ∥x∥ :=
-homothety_norm _ (to_span_singleton_homothety 𝕜 x)
-
 variable (f)
 
 theorem uniform_embedding_of_bound {K : ℝ≥0} (hf : ∀ x, ∥x∥ ≤ K * ∥f x∥) :