det_fintype — Mathlib

English

If the index α is finite, the determinant of a block-triangular matrix equals the product, over all blocks, of the determinants of the diagonal blocks M^{(b)}_k.

Русский

Если индекс α конечен, детерминант блочно-верхнетреугольной матрицы равен произведению детерминантов диагональных блоков по всем блокам.

LaTeX

$$$\det M = \prod_{k \in \alpha} \det\big(M^{(b)}_k\big)$$$

Lean4

theorem det_fintype [DecidableEq α] [Fintype α] [LinearOrder α] (h : BlockTriangular M b) :
    M.det = ∏ k : α, (M.toSquareBlock b k).det :=
  by
  refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)
  have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
  exact det_isEmpty

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