English
If a matrix M is block-triangular with respect to a partition p, the determinant factors as the product of the determinants of the two diagonal blocks M_{pp} and M_{¬p¬p}.
Русский
Если матрица M блочно-верхнетреугольна относительно разбиения p, детерминант M факторизуется в произведение детерминантов диагональных блоков M_{pp} и M_{¬p¬p}.
LaTeX
$$$\det M = \det(M_{pp}) \cdot \det(M_{\lnot p \lnot p})$$$
Lean4
theorem twoBlockTriangular_det (M : Matrix m m R) (p : m → Prop) [DecidablePred p]
(h : ∀ i, ¬p i → ∀ j, p j → M i j = 0) :
M.det = (toSquareBlockProp M p).det * (toSquareBlockProp M fun i => ¬p i).det :=
by
rw [det_toBlock M p]
convert det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) fun j => ¬p j)
ext i j
exact h (↑i) i.2 (↑j) j.2
