∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α),
  P 0 → (∀ (p q : Matrix m n α), P p → P q → P (p + q)) → (∀ (i : m) (j : n) (x : α), P (Matrix.single i j x)) → P M