trace_submatrix_succ — Mathlib

English

Let M be a square matrix of size (n+1) with entries in R. Then the trace satisfies tr(M) = M_{0,0} + tr(submatrix(M, Fin.succ, Fin.succ)).

Русский

Пусть M — квадратная матрица размера (n+1)×(n+1) над кольцом R. Тогда след выполняется как tr(M) = M_{0,0} + tr(submatrix(M, Fin.succ, Fin.succ)).

LaTeX

$$$$ \\operatorname{trace}(M) = M_{0,0} + \\operatorname{trace}(\\operatorname{submatrix}(M, \\operatorname{Fin.succ}, \\operatorname{Fin.succ})). $$$$

Lean4

theorem trace_submatrix_succ {n : ℕ} [AddCommMonoid R] (M : Matrix (Fin n.succ) (Fin n.succ) R) :
    M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M :=
  by
  delta trace
  rw [← (finSuccEquiv n).symm.sum_comp]
  simp

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