English
Induction principle for finite matrices: if P holds for 0, is closed under addition, and holds for all single i j x, then P M for any finite matrices M.
Русский
Принцип индукции по конечным матрицам: если верно P(0), P(p+q) при P(p) и P(q), и P( single i j x ) для всех i,j,x, то P(M) для любой конечной матрицы M.
LaTeX
$$$ P(M) \;\text{ follows from } P(0), \; \forall p,q\ P(p) \to P(q) \to P(p+q), \; \forall i j x\ P(single_{i j} x)$$$
Lean4
@[elab_as_elim]
protected theorem induction_on [AddCommMonoid α] [Finite m] [Finite n] [Nonempty m] [Nonempty n]
{P : Matrix m n α → Prop} (M : Matrix m n α) (h_add : ∀ p q, P p → P q → P (p + q))
(h_std_basis : ∀ i j x, P (single i j x)) : P M :=
Matrix.induction_on' M
(by
inhabit m
inhabit n
simpa using h_std_basis default default 0)
h_add h_std_basis
