Structures · Algebra

CanonicallyOrderedMul

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).

Defined in

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Shape

One type argument · adds le_mul_self, le_self_mul