Theorems · Theorem · number theory

ZLattice.covolume_eq_det_inv

∀ {ι : Type u_2} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [inst_2 : IsZLattice ℝ L]
  (b : Module.Basis ι ℤ ↥L),
  ZLattice.covolume L MeasureTheory.volume = |↑(LinearEquiv.det (Module.Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹

Defined in: Mathlib.Algebra.Module.ZLattice.Covolume
Cited by: 1 results in Mathlib
Foundations: Depth 261 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DiscreteTopology IsZLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites35

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
RingHom.idstatement · cited by 18,349
Fintypestatement and proof · cited by 7,736
Submodulestatement and proof · cited by 7,192
MonoidHomstatement · cited by 3,629
LinearEquivstatement · cited by 3,317
Unitsstatement · cited by 2,804
Units.valstatement and proof · cited by 1,966
absstatement and proof · cited by 1,814
Module.Basisstatement and proof · cited by 1,477
MeasureTheory.MeasureSpace.volumestatement · cited by 1,323

Cited by1

Results whose statement or proof uses this declaration.

ZLattice.volume_image_eq_volume_div_covolumeproof · cited by 3