case a.h
l : Type ?u.266590
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.266604
n' : o → Type ?u.266609
R : Type ?u.266612
S : Type ?u.266615
α : Type v
β : Type w
γ : Type ?u.266622
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
x✝ : o
⊢ (L ⬝ (M + N)) i✝ x✝ = (L ⬝ M + L ⬝ N) i✝ x✝
l : Type ?u.266590
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.266604
n' : o → Type ?u.266609
R : Type ?u.266612
S : Type ?u.266615
α : Type v
β : Type w
γ : Type ?u.266622
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L ⬝ (M + N) = L ⬝ M + L ⬝ N
ext
no goals
case a.h
l : Type ?u.266590
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.266604
n' : o → Type ?u.266609
R : Type ?u.266612
S : Type ?u.266615
α : Type v
β : Type w
γ : Type ?u.266622
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
x✝ : o
⊢ (L ⬝ (M + N)) i✝ x✝ = (L ⬝ M + L ⬝ N) i✝ x✝
apply dotProduct_add