Theorems · Inductive type · order theory
MulArchimedean
(R : Type u_2) → [CommMonoid R] → [PartialOrder R] → Prop
An ordered commutative monoid is called MulArchimedean if for any two elements x, y
such that 1 < y, there exists a natural number n such that x ≤ y ^ n.
- Defined in
- Mathlib.Algebra.Order.Archimedean.Defs
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommMonoidPartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement · cited by 6,410
- CommMonoidstatement · cited by 2,264
Cited by48
Results whose statement or proof uses this declaration.
- MulArchimedean.archstatement and proof · cited by 5
- MulArchimedean.comapstatement and proof · cited by 5
- LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrderedstatement and proof · cited by 4
- existsUnique_zpow_near_of_one_ltstatement and proof · cited by 3
- Subgroup.cyclic_of_minstatement and proof · cited by 2
- Subgroup.dense_of_not_isolated_onestatement and proof · cited by 2
- Subgroup.dense_or_cyclicstatement and proof · cited by 2
- Subgroup.dense_xor_cyclicstatement and proof · cited by 2
- existsUnique_add_zpow_mem_Iocstatement and proof · cited by 2
- existsUnique_zpow_near_of_one_lt'statement and proof · cited by 2
- Subgroup.exists_isLeast_one_ltstatement and proof · cited by 2
- OrderMonoidIso.mulArchimedeanstatement and proof · cited by 2