Theorems · Theorem · number theory
ZSpan.volume_real_fundamentalDomain
∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (b : Module.Basis ι ℝ (ι → ℝ)),
MeasureTheory.volume.real (ZSpan.fundamentalDomain b) = |(Matrix.of ⇑b).det|- Defined in
- Mathlib.Algebra.Module.ZLattice.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Realstatement and proof · cited by 25,697
- Equivstatement · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- Matrixstatement · cited by 4,303
- absstatement and proof · cited by 1,814
- Module.Basisstatement and proof · cited by 1,477
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- ENNReal.toRealproof · cited by 859
- Matrix.detstatement and proof · cited by 665
- MeasureTheory.Measure.realstatement · cited by 530
- Matrix.ofstatement and proof · cited by 336
Cited by1
Results whose statement or proof uses this declaration.
- ZLattice.covolume_eq_detproof · cited by 3