English
Induction on a finite matrix: if a property P holds for 0, is closed under addition, and holds for all single i j x, then P holds for every matrix M.
Русский
Индукция по конечной матрице: если свойство P верно для нулевой матрицы, сохраняется при сложении и верно для всех элементарных матриц single i j x, то P верно для любой матрицы M.
LaTeX
$$$ P(0) \quad\land\quad (\forall p,q, P(p) \to P(q) \to P(p+q)) \quad\land\quad (\forall i j x, P(\mathrm{single}_{i j} x)) \Rightarrow P(M) $$$
Lean4
@[elab_as_elim]
protected theorem induction_on' [AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α)
(h_zero : P 0) (h_add : ∀ p q, P p → P q → P (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)) :
P M := by
cases nonempty_fintype m; cases nonempty_fintype n
rw [matrix_eq_sum_single M, ← Finset.sum_product']
apply Finset.sum_induction _ _ h_add h_zero
· intros
apply h_std_basis
