Theorems · Definition · number theory
approxOrderOf
(A : Type u_1) → [SeminormedGroup A] → ℕ → ℝ → Set A
In a seminormed group A, given n : ℕ and δ : ℝ, approxOrderOf A n δ is the set of
elements within a distance δ of a point of order n.
- Defined in
- Mathlib.NumberTheory.WellApproximable
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- orderOfproof · cited by 324
- SeminormedGroupstatement and proof · cited by 250
- Metric.thickeningproof · cited by 130
Cited by7
Results whose statement or proof uses this declaration.
- mem_approxOrderOf_iffstatement · cited by 2
- wellApproximableproof · cited by 1
- mem_wellApproximable_iffstatement · cited by 0
- approxOrderOf.image_pow_subsetstatement and proof · cited by 0
- approxOrderOf.image_pow_subset_of_coprimestatement and proof · cited by 0
- approxOrderOf.smul_eq_of_mul_dvdstatement · cited by 0
- approxOrderOf.smul_subset_of_coprimestatement · cited by 0