Theorems · Definition · number theory
ZLattice.covolume
{E : Type u_1} →
[inst : NormedAddCommGroup E] →
[inst_1 : MeasurableSpace E] → Submodule ℤ E → autoParam (MeasureTheory.Measure E) ZLattice.covolume._auto_1 → ℝThe covolume of a ℤ-lattice is the volume of some fundamental domain; see
ZLattice.covolume_eq_volume for the proof that the volume does not depend on the choice of
the fundamental domain.
- Defined in
- Mathlib.Algebra.Module.ZLattice.Covolume
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Submodulestatement and proof · cited by 7,192
- ENNReal.toRealproof · cited by 859
- MeasureTheory.addCovolumeproof · cited by 5
Cited by23
Results whose statement or proof uses this declaration.
- NumberField.Units.regulatorproof · cited by 19
- NumberField.Units.regOfFamilyproof · cited by 12
- NumberField.Units.regulator_eq_regOfFamily_fundSystemproof · cited by 7
- ZLattice.covolume_eq_measure_fundamentalDomainstatement · cited by 6
- ZLattice.covolume_posstatement · cited by 5
- NumberField.Units.regOfFamily_of_isMaxRankstatement and proof · cited by 4
- ZLattice.covolume_comapstatement and proof · cited by 3
- ZLattice.covolume_eq_detstatement · cited by 3
- ZLattice.volume_image_eq_volume_div_covolumestatement and proof · cited by 3
- ZLattice.covolume_div_covolume_eq_relIndexstatement and proof · cited by 2
- ZLattice.volume_image_eq_volume_div_covolume'statement and proof · cited by 2
- ZLattice.covolume.tendsto_card_le_div'statement and proof · cited by 1