l : Type ?u.21103
m : Type u_1
n : Type u_2
R : Type ?u.21112
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
l : Type ?u.21103
m : Type u_1
n : Type u_2
R : Type ?u.21112
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ stdBasisMatrix i j c i' j' = 0
simp only [stdBasisMatrix, and_imp, ite_eq_right_iff]
no goals
l : Type ?u.21103
m : Type u_1
n : Type u_2
R : Type ?u.21112
α : Type u_3
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
tauto