case a.h
l : Type ?u.1225606
m : Type u_2
n : Type u_1
o : Type ?u.1225615
m' : o → Type ?u.1225620
n' : o → Type ?u.1225625
R : Type ?u.1225628
S : Type ?u.1225631
α : Type v
β : Type w
γ : Type ?u.1225638
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ updateRow Mᵀ j c i✝ x✝ = (updateColumn M j c)ᵀ i✝ x✝
l : Type ?u.1225606
m : Type u_2
n : Type u_1
o : Type ?u.1225615
m' : o → Type ?u.1225620
n' : o → Type ?u.1225625
R : Type ?u.1225628
S : Type ?u.1225631
α : Type v
β : Type w
γ : Type ?u.1225638
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
⊢ updateRow Mᵀ j c = (updateColumn M j c)ᵀ
ext
case a.h
l : Type ?u.1225606
m : Type u_2
n : Type u_1
o : Type ?u.1225615
m' : o → Type ?u.1225620
n' : o → Type ?u.1225625
R : Type ?u.1225628
S : Type ?u.1225631
α : Type v
β : Type w
γ : Type ?u.1225638
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ (if i✝ = j then c x✝ else Mᵀ i✝ x✝) = if i✝ = j then c x✝ else M x✝ i✝
case a.h
l : Type ?u.1225606
m : Type u_2
n : Type u_1
o : Type ?u.1225615
m' : o → Type ?u.1225620
n' : o → Type ?u.1225625
R : Type ?u.1225628
S : Type ?u.1225631
α : Type v
β : Type w
γ : Type ?u.1225638
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ updateRow Mᵀ j c i✝ x✝ = (updateColumn M j c)ᵀ i✝ x✝
rw [transpose_apply, updateRow_apply, updateColumn_apply]
no goals
case a.h
l : Type ?u.1225606
m : Type u_2
n : Type u_1
o : Type ?u.1225615
m' : o → Type ?u.1225620
n' : o → Type ?u.1225625
R : Type ?u.1225628
S : Type ?u.1225631
α : Type v
β : Type w
γ : Type ?u.1225638
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
i✝ : n
x✝ : m
⊢ (if i✝ = j then c x✝ else Mᵀ i✝ x✝) = if i✝ = j then c x✝ else M x✝ i✝
rfl