English
For a lattice L with a basis b and another basis b0, covolume is the product of the absolute determinant of the change-of-basis matrix and the real-measure of the fundamental domain of b0.
Русский
Для решетки L с базисами b и b0 коволюм равен произведению модуля детерминанта матрицы смены базиса на действительную меру фундаментальной области b0.
LaTeX
$$$\\operatorname{covolume}(L,\\mu) = \\big|\\det((\\uparrow) \\circ b)\\big| \\cdot \\mu_{\\mathbb{R}}(\\operatorname{fundamentalDomain}(b_0))$$$
Lean4
theorem covolume_eq_det_mul_measureReal {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ L) (b₀ : Basis ι ℝ E) :
covolume L μ = |b₀.det ((↑) ∘ b)| * μ.real (fundamentalDomain b₀) :=
by
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ), measureReal_fundamentalDomain _ _ b₀,
measureReal_congr (fundamentalDomain_ae_parallelepiped b₀ μ)]
congr
ext
exact b.ofZLatticeBasis_apply ℝ L _
