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 AddSubgroup 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 : AddSubgroup (ι)) [DiscreteTopology L] [IsZlattice L] (b : Basis ι L) :
    Zlattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val b)).det|