Canonically ordered monoids #
For
a ≤ b≤ b
,a
left dividesb
An OrderCommMonoid
with one-sided 'division' in the sense that
if a ≤ b≤ b
, there is some c
for which a * c = b
. This is a weaker version
of the condition on canonical orderings defined by CanonicallyOrderedMonoid
.
Instances
For
a ≤ b≤ b
, there is ac
sob = a + c
.
An OrderAddCommMonoid
with one-sided 'subtraction' in the sense that
if a ≤ b≤ b
, then there is some c
for which a + c = b
. This is a weaker version
of the condition on canonical orderings defined by CanonicallyOrderedAddMonoid
.
Instances
Equations
- (_ : ExistsAddOfLE α) = (_ : ExistsAddOfLE α)
⊥⊥
is the least elementFor
a ≤ b≤ b
, there is ac
sob = a + c
.For any
a
andb
,a ≤ a + b≤ a + b
A canonically ordered additive monoid is an ordered commutative additive monoid
in which the ordering coincides with the subtractibility relation,
which is to say, a ≤ b≤ b
iff there exists c
with b = a + c
.
This is satisfied by the natural numbers, for example, but not
the integers or other nontrivial OrderedAddCommGroup
s.
Instances
Equations
- CanonicallyOrderedAddMonoid.toOrderBot α = OrderBot.mk (_ : ∀ (x : α), ⊥ ≤ x)
⊥⊥
is the least elementFor
a ≤ b≤ b
, there is ac
sob = a * c
.For any
a
andb
,a ≤ a * b≤ a * b
A canonically ordered monoid is an ordered commutative monoid
in which the ordering coincides with the divisibility relation,
which is to say, a ≤ b≤ 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).
Instances
Equations
- CanonicallyOrderedMonoid.toOrderBot α = OrderBot.mk (_ : ∀ (x : α), ⊥ ≤ x)
Equations
- (_ : ExistsAddOfLE α) = (_ : ExistsAddOfLE α)
Equations
Equations
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.
A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.
Instances
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.
A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
In a linearly ordered monoid, we are happy for bot_eq_zero
to be a @[simp]
lemma
In a linearly ordered monoid, we are happy for bot_eq_one
to be a @[simp]
lemma.