Theorems · Inductive type · number theory

IsZLattice

(K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace K E] → (L : Submodule ℤ E) → [DiscreteTopology ↥L] → Prop

L : Submodule ℤ E where E is a vector space over a normed field K is a ℤ-lattice if it is discrete and spans E over K.

Defined in: Mathlib.Algebra.Module.ZLattice.Basic
Cited by: 32 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedField NormedAddCommGroup NormedSpace DiscreteTopology

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

NormedAddCommGroupstatement · cited by 15,752
NormedSpacestatement · cited by 12,499
Submodulestatement · cited by 7,192
NormedFieldstatement · cited by 1,084
DiscreteTopologystatement · cited by 373

Cited by36

Results whose statement or proof uses this declaration.

Module.Basis.ofZLatticeBasisstatement and proof · cited by 36
Module.Basis.ofZLatticeBasis_applystatement and proof · cited by 11
ZLattice.covolume_eq_measure_fundamentalDomainstatement and proof · cited by 6
Module.Basis.ofZLatticeBasis_spanstatement and proof · cited by 6
ZLattice.covolume_posstatement and proof · cited by 5
ZLattice.rankstatement and proof · cited by 5
ZLattice.isAddFundamentalDomainstatement and proof · cited by 4
Module.Basis.ofZLatticeBasis_repr_applystatement and proof · cited by 4
ZLattice.covolume_comapstatement and proof · cited by 3
ZLattice.covolume_eq_detstatement and proof · cited by 3
ZLattice.module_finitestatement and proof · cited by 3
ZLattice.volume_image_eq_volume_div_covolumestatement and proof · cited by 3