Theorems · Inductive type · order theory
CanonicallyOrderedMul
(α : Type u_1) → [Mul α] → [LE α] → Prop
An ordered monoid is CanonicallyOrderedMul
if the ordering coincides with the divisibility relation,
which is to say, a ≤ b iff there exists c with b = a * c.
Examples seem rare; it seems more likely that the OrderDual
of a naturally-occurring lattice satisfies this than the lattice
itself (for example, dual of the lattice of ideals of a PID or
Dedekind domain satisfy this; collections of all things ≤ 1 seem to
be more natural that collections of all things ≥ 1).
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 1 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 by54
Results whose statement or proof uses this declaration.
- le_self_mulstatement and proof · cited by 5
- CanonicallyOrderedMul.toIsOrderedMonoidstatement and proof · cited by 5
- le_mul_selfstatement and proof · cited by 4
- le_iff_exists_mulstatement and proof · cited by 4
- Finset.prod_le_prod_of_subset'statement and proof · cited by 3
- Finset.prod_mono_set'statement and proof · cited by 2
- Submonoid.fg_of_divisivestatement and proof · cited by 2
- le_mul_leftstatement · cited by 1
- le_mul_of_le_leftstatement and proof · cited by 1
- le_mul_of_le_rightstatement and proof · cited by 1
- self_le_mul_rightstatement and proof · cited by 1
- le_mul_rightstatement · cited by 1