∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : α → β),
  (Matrix.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)