Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

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.

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

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
    theorem ExistsAddOfLE.exists_add_of_le {α : Type u} [Add α] [LE α] [self : ExistsAddOfLE α] {a : α} {b : α} :
    a b∃ (c : α), b = a + c

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

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

    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
      theorem ExistsMulOfLE.exists_mul_of_le {α : Type u} [Mul α] [LE α] [self : ExistsMulOfLE α] {a : α} {b : α} :
      a b∃ (c : α), b = a * c

      For a ≤ b, a left divides b

      @[instance 100]
      instance AddGroup.existsAddOfLE (α : Type u) [AddGroup α] [LE α] :
      Equations
      • =
      @[instance 100]
      instance Group.existsMulOfLE (α : Type u) [Group α] [LE α] :
      Equations
      • =
      theorem exists_nonneg_add_of_le {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : a b) :
      ∃ (c : α), 0 c a + c = b
      theorem exists_one_le_mul_of_le {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : a b) :
      ∃ (c : α), 1 c a * c = b
      theorem exists_pos_add_of_lt' {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (h : a < b) :
      ∃ (c : α), 0 < c a + c = b
      theorem exists_one_lt_mul_of_lt' {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] (h : a < b) :
      ∃ (c : α), 1 < c a * c = b
      theorem le_iff_exists_nonneg_add {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
      a b ∃ (c : α), 0 c a + c = b
      theorem le_iff_exists_one_le_mul {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
      a b ∃ (c : α), 1 c a * c = b
      theorem lt_iff_exists_pos_add {α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
      a < b ∃ (c : α), 0 < c a + c = b
      theorem lt_iff_exists_one_lt_mul {α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
      a < b ∃ (c : α), 1 < c a * c = b
      theorem le_of_forall_pos_le_add {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa b + ε) :
      a b
      theorem le_of_forall_one_lt_le_mul {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa b * ε) :
      a b
      theorem le_of_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
      a b
      theorem le_of_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
      a b
      theorem le_iff_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
      a b ∀ (ε : α), 0 < εa < b + ε
      theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
      a b ∀ (ε : α), 1 < εa < b * ε