det_pi — Mathlib

English

For a finite index set ι, the determinant of the block-diagonal operator given by the family f i equals the product of the determinants of each fi.

Русский

Для конечного множества индексов ι детерминант блочно диагонального оператора, заданного семейством fi, равен произведению детерминант каждой fi.

LaTeX

$$$\bigl(\mathrm{pi}\, i \mapsto (f_i).\mathrm{comp}(\mathrm{proj}_i)\bigr).\mathrm{det} = \prod_i (f_i).\mathrm{det}$$$

Lean4

theorem det_pi {ι R M : Type*} [Fintype ι] [CommRing R] [AddCommGroup M] [TopologicalSpace M] [Module R M]
    [Module.Free R M] [Module.Finite R M] (f : ι → M →L[R] M) :
    (pi (fun i ↦ (f i).comp (proj i))).det = ∏ i, (f i).det :=
  LinearMap.det_pi _

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