R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
⊢ ∑ i : n, ∑ j : m, v i * M i j * w j = ∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
⊢ ↑(↑(↑toLinearMap₂' M) v) w = v ⬝ᵥ mulVec M w
simp_rw [Matrix.toLinearMap₂'_apply, Matrix.dotProduct, Matrix.mulVec, Matrix.dotProduct]
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ * M x✝¹ j * w j = v x✝¹ * ∑ x : m, M x✝¹ x * w x
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
⊢ ∑ i : n, ∑ j : m, v i * M i j * w j = ∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1
refine' Finset.sum_congr rfl fun _ _ => _
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ * M x✝¹ j * w j = ∑ x : m, v x✝¹ * (M x✝¹ x * w x)
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ * M x✝¹ j * w j = v x✝¹ * ∑ x : m, M x✝¹ x * w x
rw [Finset.mul_sum]
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ * M x✝³ x✝¹ * w x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ * M x✝¹ j * w j = ∑ x : m, v x✝¹ * (M x✝¹ x * w x)
refine' Finset.sum_congr rfl fun _ _ => _
no goals
R : Type u_3
R₁ : Type ?u.308004
R₂ : Type ?u.308007
M✝ : Type ?u.308010
M₁ : Type ?u.308013
M₂ : Type ?u.308016
M₁' : Type ?u.308019
M₂' : Type ?u.308022
n : Type u_1
m : Type u_2
n' : Type ?u.308031
m' : Type ?u.308034
ι : Type ?u.308037
inst✝⁶ : CommRing R
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
M : Matrix n m R
v : n → R
w : m → R
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ * M x✝³ x✝¹ * w x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
rw [← mul_assoc]