golf

leanprover-community · Jan 22, 2025 · 36fff08 · 36fff08
1 parent 65e8fba
commit 36fff08
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Mathlib/Data/Matrix/Mul.lean b/Mathlib/Data/Matrix/Mul.lean
@@ -646,9 +646,8 @@ theorem vecMul_eq_sum [Fintype m] (v : m → α) (M : Matrix m n α) : v ᵥ* M
   (Finset.sum_fn ..).symm
 
 theorem mulVec_eq_sum [Fintype n] (v : n → α) (M : Matrix m n α) :
-    M *ᵥ v = ∑ i, MulOpposite.op (v i) • Mᵀ i := by
-  ext i
-  simp [show (M *ᵥ v) i = ∑ x, M i x * v x from rfl]
+    M *ᵥ v = ∑ i, MulOpposite.op (v i) • Mᵀ i :=
+  funext fun i ↦ by simp [show (M *ᵥ v) i = ∑ x, M i x * v x from rfl]
 
 theorem mulVec_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
     (diagonal v *ᵥ w) x = v x * w x :=