twoBlockTriangular_det' — Mathlib

English

Under the same hypotheses as above, the determinant equals the product of the determinants of the two diagonal blocks M_{pp} and M_{¬p¬p}, possibly with a different presentation of the blocks.

Русский

При тех же гипотезах детерминант равен произведению детерминантов диагональных блоков 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 [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]
  · congr 1
    exact equiv_block_det _ fun _ => not_not.symm
  · simpa only [Classical.not_not] using h

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