Theorems · Theorem · number theory

ZLattice.covolume_comap

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_28✝) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℝ F] [FiniteDimensional ℝ F] [inst_11 : MeasurableSpace F]
  [BorelSpace F] (ν : autoParam (MeasureTheory.Measure F) ZLattice.covolume_comap._auto_1) [ν.IsAddHaarMeasure]
  {e : F ≃L[ℝ] E},
  MeasureTheory.MeasurePreserving (⇑e) ν μ → ZLattice.covolume (ZLattice.comap ℝ L ↑↑e) ν = ZLattice.covolume L μ

Defined in

Mathlib.Algebra.Module.ZLattice.Covolume

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceDiscreteTopologyIsZLatticeMeasureTheory.Measure.IsAddHaarMeasureNormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure