English
The covolume is the reciprocal of the determinant of the lattice-basis change map when expressed as a linear isomorphism.
Русский
Коволюм равен обратному детерминанту отображения смены базиса решетки, если рассматривать как линейное изоморщество.
LaTeX
$$$\\operatorname{covolume}(L,\\mu) = \\left| \\det\\big( (b_{\\mathrm{ofZLatticeBasis}\\, \\mathbb{R}}\\; L) .\\mathrm{equivFun} \\big) \\right|^{-1}$$$
Lean4
theorem covolume_eq_det_inv {ι : Type*} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L] [IsZLattice ℝ L]
(b : Basis ι ℤ L) : covolume L = |(LinearEquiv.det (b.ofZLatticeBasis ℝ L).equivFun : ℝ)|⁻¹ := by
classical
rw [covolume_eq_det L b, ← Pi.basisFun_det_apply, show (((↑) : L → _) ∘ ⇑b) = (b.ofZLatticeBasis ℝ) by ext; simp, ←
Basis.det_inv, ← abs_inv, Units.val_inv_eq_inv_val, IsUnit.unit_spec, ← Basis.det_basis, LinearEquiv.coe_det]
rfl
