∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] (f : α →+* β) (M : Matrix m m α), M.map ⇑f = f.mapMatrix M