Theorems · Theorem · order theory
existsUnique_zpow_near_of_one_lt
∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
1 < a → ∀ (g : G), ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)An archimedean decidable linearly ordered CommGroup has a version of the floor: for
a > 1, any g in the group lies between some two consecutive powers of a.
- Defined in
- Mathlib.Algebra.Order.Archimedean.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- LinearOrderstatement and proof · cited by 8,572
- Set.ofPredproof · cited by 6,101
- Set.Nonemptyproof · cited by 2,627
- CommGroupstatement and proof · cited by 990
- le_transproof · cited by 985
- IsOrderedMonoidstatement and proof · cited by 577
- LE.le.antisymmproof · cited by 507
- inv_invproof · cited by 494
- lt_of_le_of_ltproof · cited by 432
- zpow_natCastproof · cited by 271
- ExistsUniquestatement · cited by 268
Cited by3
Results whose statement or proof uses this declaration.
- existsUnique_add_zpow_mem_Iocproof · cited by 2
- existsUnique_zpow_near_of_one_lt'proof · cited by 2
- Subgroup.cyclic_of_minproof · cited by 2