∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : AddZeroClass α]
  (i : m) (j : n) (a b : α), Matrix.single i j (a + b) = Matrix.single i j a + Matrix.single i j b