style(analysis/inner_product_space/l2_space): small style improvement (…

…#15698) Spotted by @hrmacbeth
leanprover-community · Jul 26, 2022 · 10aeb39 · 10aeb39
1 parent 8050ac7
commit 10aeb39
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/analysis/inner_product_space/l2_space.lean b/src/analysis/inner_product_space/l2_space.lean
@@ -391,9 +391,9 @@ end
 protected lemma has_sum_inner_mul_inner (b : hilbert_basis ι 𝕜 E) (x y : E) :
   has_sum (λ i, ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫ :=
 begin
-  convert (b.has_sum_repr y).map _ (innerSL x).continuous,
+  convert (b.has_sum_repr y).mapL (innerSL x),
   ext i,
-  rw [function.comp_apply, innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
+  rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
 end
 
 protected lemma summable_inner_mul_inner (b : hilbert_basis ι 𝕜 E) (x y : E) :