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