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

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

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

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