l : Type ?u.3365
m : Type u_1
n : Type u_2
R : Type ?u.3374
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ (fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0
l : Type ?u.3365
m : Type u_1
n : Type u_2
R : Type ?u.3374
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 0 = 0
unfold stdBasisMatrix
case a.h
l : Type ?u.3365
m : Type u_1
n : Type u_2
R : Type ?u.3374
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then 0 else 0) = OfNat.ofNat 0 i✝ x✝
l : Type ?u.3365
m : Type u_1
n : Type u_2
R : Type ?u.3374
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ (fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0
ext
no goals
case a.h
l : Type ?u.3365
m : Type u_1
n : Type u_2
R : Type ?u.3374
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then 0 else 0) = OfNat.ofNat 0 i✝ x✝
simp