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 _))