case a.h
l : Type ?u.41930
m : Type ?u.41933
n : Type u_1
R : Type ?u.41939
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (stdBasisMatrix i j c ⬝ stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
l : Type ?u.41930
m : Type ?u.41933
n : Type u_1
R : Type ?u.41939
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
⊢ stdBasisMatrix i j c ⬝ stdBasisMatrix j k d = stdBasisMatrix i k (c * d)
ext (a b)
case a.h
l : Type ?u.41930
m : Type ?u.41933
n : Type u_1
R : Type ?u.41939
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
case a.h
l : Type ?u.41930
m : Type ?u.41933
n : Type u_1
R : Type ?u.41939
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (stdBasisMatrix i j c ⬝ stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
simp only [mul_apply, stdBasisMatrix, boole_mul]
no goals
case a.h
l : Type ?u.41930
m : Type ?u.41933
n : Type u_1
R : Type ?u.41939
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
by_cases h₁ : i = a <;> by_cases h₂ : k = b <;> simp [h₁, h₂]