Theorems · Theorem · number theory

ZSpan.isAddFundamentalDomain

∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι] [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E),
  MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b))) (ZSpan.fundamentalDomain b) μ

For a ℤ-lattice Submodule.span ℤ (Set.range b), proves that the set defined by ZSpan.fundamentalDomain is a fundamental domain.

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

5 results in Mathlib

Foundations

Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteMeasurableSpaceOpensMeasurableSpace