single_apply_same — Mathlib

English

Standard induction on finite matrices: if P is stable under addition and holds on standard basis and zero, then P holds for all finite matrices.

Русский

Стандартная индукция по конечным матрицам: если P сохраняется при сложении, и верна для базиса и нуля, то P верна для любой конечной матрицы.

LaTeX

$$$ P(0) \land (\forall p,q, P(p) \to P(q) \to P(p+q)) \land (\forall i j x, P(single i j x)) \Rightarrow P(M) $$$

Lean4

@[simp]
theorem single_apply_same : single i j c i j = c :=
  if_pos (And.intro rfl rfl)

Похожие утверждения