det — Mathlib

English

A restatement of two-block triangular determinant: the determinant factors as the product of the determinants of the diagonal blocks corresponding to p and its complement.

Русский

Переформулировка: детерминант блочно-верхнетреугольной матрицы делится на произведение детерминантов диагональных блоков, соответствующих p и его дополнению.

LaTeX

$$$\det M = \det(M_{pp}) \cdot \det(M_{\lnot p \lnot p})$$$

Lean4

protected theorem det [DecidableEq α] [LinearOrder α] (hM : BlockTriangular M b) :
    M.det = ∏ a ∈ univ.image b, (M.toSquareBlock b a).det :=
  by
  suffices ∀ hs : Finset α, univ.image b = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det by exact this _ rfl
  intro s hs
  induction s using Finset.eraseInduction generalizing m with
  | H s ih =>
    subst hs
    cases isEmpty_or_nonempty m
    · simp
    let k := (univ.image b).max' (univ_nonempty.image _)
    rw [twoBlockTriangular_det' M fun i => b i = k]
    · have : univ.image b = insert k ((univ.image b).erase k) :=
        by
        rw [insert_erase]
        apply max'_mem
      rw [this, prod_insert (notMem_erase _ _)]
      refine congr_arg _ ?_
      let b' := fun i : { a // b a ≠ k } => b ↑i
      have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
      have hb' : image b' univ = (image b univ).erase k := by convert image_subtype_ne_univ_eq_image_erase k b
      rw [ih _ (max'_mem _ _) h' hb']
      refine Finset.prod_congr rfl fun l hl => ?_
      let he : { a // b' a = l } ≃ { a // b a = l } :=
        haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
        Equiv.subtypeSubtypeEquivSubtype @(hc)
      simp only [toSquareBlock_def]
      erw [← Matrix.det_reindex_self he.symm fun i j : { a // b a = l } => M ↑i ↑j]
      rfl
    · intro i hi j hj
      apply hM
      rw [hi]
      apply lt_of_le_of_ne _ hj
      exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

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