det_toSquareBlock_id — Mathlib

English

Let M be a square matrix indexed by a finite set. For each index i, consider the i-th diagonal block of M with respect to the identity partition. Then the determinant of that block equals the i,i entry of M.

Русский

Пусть M — квадратная матрица, индексированная по конечному множеству. Для каждого индекса i рассмотрим i-й диагональный блок M относительно тождественного разбиения. Детерминант этого блока равен M_{ii}.

LaTeX

$$$\det\big(M^{(\mathrm{id})}_{ii}\big) = M_{ii}$$$

Lean4

theorem det_toSquareBlock_id (M : Matrix m m R) (i : m) : (M.toSquareBlock id i).det = M i i :=
  letI : Unique { a // id a = i } := ⟨⟨⟨i, rfl⟩⟩, fun j => Subtype.ext j.property⟩
  (det_unique _).trans rfl

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