English
Let M be a square matrix and p a partition of the index set into two parts. Then the determinant of M is equal to the determinant of the 2-by-2 block matrix formed by the four blocks M_{pp}, M_{p\neg p}, M_{\neg p p}, M_{\neg p \neg p}.
Русский
Пусть M — квадратная матрица, а множество индексов разбито на две части p и ее дополнение. Тогда детерминант M равен детерминанту блочно-матрицы 2×2, составленной из блоков M_{pp}, M_{p\not p}, M_{\not p p}, M_{\not p \not p}.
LaTeX
$$$\det M = \det\begin{pmatrix} M_{pp} & M_{p\neg p} \\ M_{\neg p p} & M_{\neg p \neg p} \end{pmatrix}$$$
Lean4
theorem det_toBlock (M : Matrix m m R) (p : m → Prop) [DecidablePred p] :
M.det =
(fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p) <|
toBlock M (fun j => ¬p j) fun j => ¬p j).det :=
by
rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]
rw [det_apply', det_apply']
congr; ext σ; congr; ext x
generalize hy : σ x = y
cases x <;> cases y <;>
simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Equiv.sumCompl_apply_inl,
fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁, fromBlocks_apply₂₂, Matrix.submatrix_apply]
