R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ vecMul (↑(LinearMap.stdBasis R (fun x => R) i) 1) M j = M i j
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ vecMul (↑(LinearMap.stdBasis R (fun x => R) i) 1) M j = M i j
have : (∑ i', (if i = i' then 1 else 0) * M i' j) = M i j := by
  simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ ∑ x : m, ↑(LinearMap.stdBasis R (fun x => R) i) 1 x * M x j = M i j
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ vecMul (↑(LinearMap.stdBasis R (fun x => R) i) 1) M j = M i j
simp only [vecMul, dotProduct]
case h.e'_2.a.h.e'_5
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
⊢ ↑(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = if i = x✝ then 1 else 0
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ ∑ x : m, ↑(LinearMap.stdBasis R (fun x => R) i) 1 x * M x j = M i j
convert this
case h.e'_2.a.h.e'_5.inl
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : i = x✝
⊢ Function.update 0 i 1 x✝ = 1

case h.e'_2.a.h.e'_5.inr
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : ¬i = x✝
⊢ Function.update 0 i 1 x✝ = 0
case h.e'_2.a.h.e'_5
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
⊢ ↑(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = if i = x✝ then 1 else 0
split_ifs with h <;> simp only [stdBasis_apply]
no goals
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
no goals
case h.e'_2.a.h.e'_5.inl
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : i = x✝
⊢ Function.update 0 i 1 x✝ = 1
rw [h, Function.update_same]
no goals
case h.e'_2.a.h.e'_5.inr
R : Type u_3
inst✝² : Semiring R
l : Type ?u.4510
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : ¬i = x✝
⊢ Function.update 0 i 1 x✝ = 0
rw [Function.update_noteq (Ne.symm h), Pi.zero_apply]