case h
l : Type ?u.281699
m : Type ?u.281702
n : Type u_1
o : Type ?u.281708
m' : o → Type ?u.281713
n' : o → Type ?u.281718
R : Type ?u.281721
S : Type ?u.281724
α : Type v
β : Type w
γ : Type ?u.281731
inst✝ : NonUnitalNonAssocSemiring α
a b : n → α
x✝ : n
⊢ diag (col a ⬝ row b) x✝ = (a * b) x✝
l : Type ?u.281699
m : Type ?u.281702
n : Type u_1
o : Type ?u.281708
m' : o → Type ?u.281713
n' : o → Type ?u.281718
R : Type ?u.281721
S : Type ?u.281724
α : Type v
β : Type w
γ : Type ?u.281731
inst✝ : NonUnitalNonAssocSemiring α
a b : n → α
⊢ diag (col a ⬝ row b) = a * b
ext
no goals
case h
l : Type ?u.281699
m : Type ?u.281702
n : Type u_1
o : Type ?u.281708
m' : o → Type ?u.281713
n' : o → Type ?u.281718
R : Type ?u.281721
S : Type ?u.281724
α : Type v
β : Type w
γ : Type ?u.281731
inst✝ : NonUnitalNonAssocSemiring α
a b : n → α
x✝ : n
⊢ diag (col a ⬝ row b) x✝ = (a * b) x✝
simp [Matrix.mul_apply, col, row]