Theorem: mulVec_eq_sum (Matroid/ForMathlib/LinearAlgebra/Matrix/ToLin.lean)

State before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
⊢ M *ᵥ x = ∑ i : n, x i • fun x => M x i
Tactic:
ext j
State after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = (∑ i : n, x i • fun x => M x i) j

State before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = (∑ i : n, x i • fun x => M x i) j
Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_comm]
State after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = ∑ x_1 : n, M j x_1 * x x_1

State before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = ∑ x_1 : n, M j x_1 * x x_1
Tactic:
rfl
State after:
no goals