no goals
l : Type ?u.1247421
m : Type u_1
n : Type u_2
o : Type u_3
m' : o → Type ?u.1247435
n' : o → Type ?u.1247440
R : Type ?u.1247443
S : Type ?u.1247446
α : Type v
β : Type w
γ : Type ?u.1247453
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
M : Matrix m n α
N : Matrix n o α
i : m
j : o
f : α →+* β
⊢ ↑f ((M ⬝ N) i j) = (map M ↑f ⬝ map N ↑f) i j
simp [Matrix.mul_apply, map_sum]