covolume_eq_det — Mathlib

English

For a lattice L with basis b, covolume equals the absolute determinant of the associated change-of-basis map.

Русский

Для решетки L с базисом b коволюм равен абсолютному значению детерминанта соответствующего отображения смены базиса.

LaTeX

$$$\\operatorname{covolume}(L,\\mu) = \\big| \\det\\big( (\\uparrow) \\circ b \\big) \\big|$$$

Lean4

theorem covolume_eq_det {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (b : Basis ι ℤ L) : covolume L = |(Matrix.of ((↑) ∘ b)).det| :=
  by
  rw [covolume_eq_measure_fundamentalDomain L volume (isAddFundamentalDomain b volume), volume_real_fundamentalDomain]
  congr
  ext1
  exact b.ofZLatticeBasis_apply ℝ L _

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