Theorems · Definition · number theory

ZLattice.normBound

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [FiniteDimensional ℝ E] → {L : Submodule ℤ E} → [DiscreteTopology ↥L] → {ι : Type u_3} → Module.Basis ι ℤ ↥L → ℝ

Given a basis of a (possibly not full rank) ℤ-lattice, there exists a ε > 0 such that |b.repr x i| < n for all ‖x‖ < n * ε (i.e. b.repr x i = O(x) depending only on b). This is an arbitrary choice of such an ε.

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

8 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology