Documentation

Mathlib.Algebra.Module.ZLattice.Covolume

Covolume of ℤ-lattices #

Let E be a finite dimensional real vector space with an inner product.

Let L be a -lattice L defined as a discrete -submodule of E that spans E over .

Main definitions and results #

The covolume of a -lattice is the volume of some fundamental domain; see ZLattice.covolume_eq_volume for the proof that the volume does not depend on the choice of the fundamental domain.

Equations
Instances For
    theorem ZLattice.covolume_eq_det {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule (ι)) [DiscreteTopology L] [IsZLattice L] (b : Basis ι L) :
    ZLattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val b)).det|