Theorems · Theorem · number theory

ZLattice.exists_forall_abs_repr_le_norm

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
  [DiscreteTopology ↥L] {ι : Type u_2} (b : Module.Basis ι ℤ ↥L),
  ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology