case a.h
l : Type ?u.329269
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.329283
n' : o → Type ?u.329288
R : Type ?u.329291
S : Type ?u.329294
α : Type v
β : Type w
γ : Type ?u.329301
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
i✝ : m
x✝ : o
⊢ map (L ⬝ M) (↑f) i✝ x✝ = (map L ↑f ⬝ map M ↑f) i✝ x✝
l : Type ?u.329269
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.329283
n' : o → Type ?u.329288
R : Type ?u.329291
S : Type ?u.329294
α : Type v
β : Type w
γ : Type ?u.329301
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
⊢ map (L ⬝ M) ↑f = map L ↑f ⬝ map M ↑f
ext
no goals
case a.h
l : Type ?u.329269
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.329283
n' : o → Type ?u.329288
R : Type ?u.329291
S : Type ?u.329294
α : Type v
β : Type w
γ : Type ?u.329301
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
i✝ : m
x✝ : o
⊢ map (L ⬝ M) (↑f) i✝ x✝ = (map L ↑f ⬝ map M ↑f) i✝ x✝
simp [mul_apply, map_sum]