# Unbundled and weaker forms of canonically ordered monoids #

This file provides a Prop-valued mixin for monoids satisfying a one-sided cancellativity property, namely that there is some `c` such that `b = a + c` if `a ≤ b`. This is particularly useful for generalising statements from groups/rings/fields that don't mention negation or subtraction to monoids/semirings/semifields.

source
class ExistsAddOfLE (α : Type u) [Add α] [LE α] :
Prop

An `OrderedAddCommMonoid` with one-sided 'subtraction' in the sense that if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version of the condition on canonical orderings defined by `CanonicallyOrderedAddCommMonoid`.

- exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c

  For `a ≤ b`, there is a `c` so `b = a + c`.

Instances

source
class ExistsMulOfLE (α : Type u) [Mul α] [LE α] :
Prop

An `OrderedCommMonoid` with one-sided 'division' in the sense that if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version of the condition on canonical orderings defined by `CanonicallyOrderedCommMonoid`.

- exists_mul_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a * c

  For `a ≤ b`, `a` left divides `b`

Instances

source
@[instance 100]
instance Group.existsMulOfLE (α : Type u) [Group α] [LE α] :
ExistsMulOfLE α
source
@[instance 100]
instance AddGroup.existsAddOfLE (α : Type u) [AddGroup α] [LE α] :
ExistsAddOfLE α
source
theorem exists_one_le_mul_of_le {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftReflectLE α] (h : a ≤ b) :
∃ (c : α), 1 ≤ c ∧ a * c = b
source
theorem exists_nonneg_add_of_le {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftReflectLE α] (h : a ≤ b) :
∃ (c : α), 0 ≤ c ∧ a + c = b
source
theorem exists_one_lt_mul_of_lt' {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftReflectLT α] (h : a < b) :
∃ (c : α), 1 < c ∧ a * c = b
source
theorem exists_pos_add_of_lt' {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftReflectLT α] (h : a < b) :
∃ (c : α), 0 < c ∧ a + c = b
source
theorem le_iff_exists_one_le_mul {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftMono α] [MulLeftReflectLE α] :
a ≤ b ↔ ∃ (c : α), 1 ≤ c ∧ a * c = b
source
theorem le_iff_exists_nonneg_add {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftMono α] [AddLeftReflectLE α] :
a ≤ b ↔ ∃ (c : α), 0 ≤ c ∧ a + c = b
source
theorem lt_iff_exists_one_lt_mul {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftStrictMono α] [MulLeftReflectLT α] :
a < b ↔ ∃ (c : α), 1 < c ∧ a * c = b
source
theorem lt_iff_exists_pos_add {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftStrictMono α] [AddLeftReflectLT α] :
a < b ↔ ∃ (c : α), 0 < c ∧ a + c = b
source
theorem le_of_forall_one_lt_le_mul {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α] {a b : α} (h : ∀ (ε : α), 1 < ε → a ≤ b * ε) :
a ≤ b
source
theorem le_of_forall_pos_le_add {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} (h : ∀ (ε : α), 0 < ε → a ≤ b + ε) :
a ≤ b
source
theorem le_of_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α] {a b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) :
a ≤ b
source
theorem le_of_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) :
a ≤ b
source
theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α] {a b : α} [MulLeftStrictMono α] :
a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
source
theorem le_iff_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} [AddLeftStrictMono α] :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
source
theorem le_iff_forall_one_lt_le_mul {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α] {a b : α} [MulLeftStrictMono α] :
a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε
source
theorem le_iff_forall_pos_le_add {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} [AddLeftStrictMono α] :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε