Theorems · Theorem · number theory

ZLattice.covolume_eq_det_mul_measureReal

∀ {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_31✝) [μ.IsAddHaarMeasure] {ι : Type u_2} [inst_8 : Fintype ι]
  [inst_9 : DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (b₀ : Module.Basis ι ℝ E),
  ZLattice.covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (ZSpan.fundamentalDomain b₀)

Defined in

Mathlib.Algebra.Module.ZLattice.Covolume

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceDiscreteTopologyIsZLatticeMeasureTheory.Measure.IsAddHaarMeasureFintypeDecidableEq