Covolume of a classical lattice

Let $𝐿 \leq ℤ ℝ 𝑛$ be a complete classical lattice. The covolume of $𝐿$ is the measure of the Fundamental domain, #m/def/geo or equivalently

c o v o l (𝐿) = v o l (ℝ 𝑛 / 𝐿)

where $v o l$ is an induced measure.

Properties

Suppose $𝐿' \leq ℤ 𝐿$ is a complete sublattice. Then $c o v o l (𝐿') = | 𝐿 / 𝐿' | c o v o l (𝐿)$ .

Proof

#missing/proof

#state/develop | #lang/en | #SemBr