Theorems · Definition · order theory
MulArchimedeanOrder
Type u_1 → Type u_1
Type synonym to equip an ordered group with a new Preorder defined by the infinitesimal order
of elements. a is said less than b if b is infinitesimal comparing to a, or more precisely,
∀ n, |b|ₘ ^ n < |a|ₘ. If a and b are neither infinitesimal to each other, they are equivalent
in this order.
- Defined in
- Mathlib.Algebra.Order.Archimedean.Class
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by12
Results whose statement or proof uses this declaration.
- MulArchimedeanClassproof · cited by 81
- MulArchimedeanClass.mkproof · cited by 63
- MulArchimedeanOrder.valstatement and proof · cited by 7
- MulArchimedeanOrder.ofstatement · cited by 5
- MulArchimedeanClass.indproof · cited by 1
- MulArchimedeanOrder.le_defstatement and proof · cited by 0
- MulArchimedeanOrder.lt_defstatement and proof · cited by 0
- MulArchimedeanOrder.of_symm_eqstatement · cited by 0
- MulArchimedeanOrder.of_valstatement and proof · cited by 0
- MulArchimedeanOrder.orderHomstatement and proof · cited by 0
- MulArchimedeanOrder.val_ofstatement · cited by 0
- MulArchimedeanOrder.val_symm_eqstatement · cited by 0