case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (fun i' => if i = i' then 1 else 0) (fun j' => if j = j' then 1 else 0) i' j'
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 1 = vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0
ext i' j'
case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if i = i' ∧ j = j' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (fun i' => if i = i' then 1 else 0) (fun j' => if j = j' then 1 else 0) i' j'
simp only [stdBasisMatrix, vecMulVec, mul_ite, mul_one, mul_zero, of_apply]
case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if j = j' ∧ i = i' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if i = i' ∧ j = j' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
simp_rw [@and_comm (i = i')]
no goals
case a.h
l : Type ?u.14423
m : Type u_1
n : Type u_2
R : Type ?u.14432
α : Type ?u.14435
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if j = j' ∧ i = i' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
exact ite_and _ _ _ _