Structures · Algebra
IsZLattice
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
- Shape
- 2 explicit arguments · adds span_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- Module.Basis.ofZLatticeBasis
- Module.Basis.ofZLatticeBasis_apply
- Module.Basis.ofZLatticeBasis_span
- ZLattice.covolume_eq_measure_fundamentalDomain
- ZLattice.rank
- ZLattice.covolume_pos
- Module.Basis.ofZLatticeBasis_repr_apply
- ZLattice.isAddFundamentalDomain
- ZLattice.covolume_eq_det
- ZLattice.module_finite
- ZLattice.volume_image_eq_volume_div_covolume
- ZLattice.covolume_comap
- ZLattice.module_free
- ZLattice.covolume.tendsto_card_le_div''
- ZLattice.volume_image_eq_volume_div_covolume'
- IsZLattice.span_top
- ZLattice.covolume.tendsto_card_div_pow''
- ZLattice.covolume_div_covolume_eq_relIndex
- ZLattice.covolume_eq_det_inv
- ZLattice.covolume.tendsto_card_le_div'
- ZLattice.covolume_ne_zero
- Module.Basis.ofZLatticeBasis_comap
- IsZLattice.basis
- ZLattice.FG
- ZLattice.covolume.tendsto_card_div_pow
- Module.Basis.ofZLatticeBasis.congr_simp
- IsZLattice.isCompact_range_of_periodic
- ZLattice.covolume.tendsto_card_div_pow'
- ZLattice.covolume.tendsto_card_le_div
- ZLattice.covolume_eq_det_mul_measureReal
- instIsZLatticeComap
- ZLattice.covolume_div_covolume_eq_relIndex'
- instCountable_of_discrete_submodule
Ancestors0
No ancestors.