Theorems · Theorem · number theory
ZLattice.volume_image_eq_volume_div_covolume
∀ {ι : Type u_2} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [inst_2 : IsZLattice ℝ L]
(b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)},
MeasureTheory.volume (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
MeasureTheory.volume s / ENNReal.ofReal (ZLattice.covolume L MeasureTheory.volume)- Defined in
- Mathlib.Algebra.Module.ZLattice.Covolume
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 262 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- RingHom.idstatement and proof · cited by 18,349
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- Submodulestatement and proof · cited by 7,192
- Set.imagestatement · cited by 5,609
- LinearEquivstatement and proof · cited by 3,317
- Units.valproof · cited by 1,966
- absproof · cited by 1,814
Cited by3
Results whose statement or proof uses this declaration.
- ZLattice.volume_image_eq_volume_div_covolume'proof · cited by 2
- ZLattice.covolume.tendsto_card_le_divproof · cited by 0
- ZLattice.covolume.tendsto_card_div_powproof · cited by 0