feat(analysis/normed_space/operator_norm): remove to_span_singleton_norm (#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).

Author: fpvandoorn

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∥) :