case a.h
l : Type ?u.1226495
m : Type u_1
n : Type u_2
o : Type ?u.1226504
m' : o → Type ?u.1226509
n' : o → Type ?u.1226514
R : Type ?u.1226517
S : Type ?u.1226520
α : Type v
β : Type w
γ : Type ?u.1226527
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ updateColumn Mᵀ i b i✝ x✝ = (updateRow M i b)ᵀ i✝ x✝
l : Type ?u.1226495
m : Type u_1
n : Type u_2
o : Type ?u.1226504
m' : o → Type ?u.1226509
n' : o → Type ?u.1226514
R : Type ?u.1226517
S : Type ?u.1226520
α : Type v
β : Type w
γ : Type ?u.1226527
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
⊢ updateColumn Mᵀ i b = (updateRow M i b)ᵀ
ext
case a.h
l : Type ?u.1226495
m : Type u_1
n : Type u_2
o : Type ?u.1226504
m' : o → Type ?u.1226509
n' : o → Type ?u.1226514
R : Type ?u.1226517
S : Type ?u.1226520
α : Type v
β : Type w
γ : Type ?u.1226527
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ (if x✝ = i then b i✝ else Mᵀ i✝ x✝) = if x✝ = i then b i✝ else M x✝ i✝
case a.h
l : Type ?u.1226495
m : Type u_1
n : Type u_2
o : Type ?u.1226504
m' : o → Type ?u.1226509
n' : o → Type ?u.1226514
R : Type ?u.1226517
S : Type ?u.1226520
α : Type v
β : Type w
γ : Type ?u.1226527
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ updateColumn Mᵀ i b i✝ x✝ = (updateRow M i b)ᵀ i✝ x✝
rw [transpose_apply, updateRow_apply, updateColumn_apply]
no goals
case a.h
l : Type ?u.1226495
m : Type u_1
n : Type u_2
o : Type ?u.1226504
m' : o → Type ?u.1226509
n' : o → Type ?u.1226514
R : Type ?u.1226517
S : Type ?u.1226520
α : Type v
β : Type w
γ : Type ?u.1226527
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i✝ : n
x✝ : m
⊢ (if x✝ = i then b i✝ else Mᵀ i✝ x✝) = if x✝ = i then b i✝ else M x✝ i✝
rfl