Documentation

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Canonically ordered monoids #

class ExistsMulOfLE (α : Type u) [inst : Mul α] [inst : LE α] :
  • For a ≤ b≤ b, a left divides b

    exists_mul_of_le : ∀ {a b : α}, a bc, b = a * c

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
    class ExistsAddOfLE (α : Type u) [inst : Add α] [inst : LE α] :
    • For a ≤ b≤ b, there is a c so b = a + c.

      exists_add_of_le : ∀ {a b : α}, a bc, b = 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
      def AddGroup.existsAddOfLE.proof_1 (α : Type u_1) [inst : AddGroup α] [inst : LE α] :
      Equations
      theorem exists_pos_add_of_lt' {α : Type u} [inst : AddZeroClass α] [inst : Preorder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ExistsAddOfLE α] {a : α} {b : α} (h : a < b) :
      c, 0 < c a + c = b
      theorem exists_one_lt_mul_of_lt' {α : Type u} [inst : MulOneClass α] [inst : Preorder α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ExistsMulOfLE α] {a : α} {b : α} (h : a < b) :
      c, 1 < c a * c = b
      theorem le_of_forall_pos_le_add {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa b + ε) :
      a b
      theorem le_of_forall_one_lt_le_mul {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa b * ε) :
      a b
      theorem le_of_forall_pos_lt_add' {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
      a b
      theorem le_of_forall_one_lt_lt_mul' {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
      a b
      theorem le_iff_forall_pos_lt_add' {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a b ∀ (ε : α), 0 < εa < b + ε
      theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a b ∀ (ε : α), 1 < εa < b * ε
      • ⊥⊥ is the least element

        bot_le : ∀ (x : α), x
      • For a ≤ b≤ b, there is a c so b = a + c.

        exists_add_of_le : ∀ {a b : α}, a bc, b = a + c
      • For any a and b, a ≤ a + b≤ a + b

        le_self_add : ∀ (a b : α), a 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 OrderedAddCommGroups.

      Instances
        class CanonicallyOrderedMonoid (α : Type u_1) extends OrderedCommMonoid , Bot :
        Type u_1
        • ⊥⊥ is the least element

          bot_le : ∀ (x : α), x
        • For a ≤ b≤ b, there is a c so b = a * c.

          exists_mul_of_le : ∀ {a b : α}, a bc, b = a * c
        • For any a and b, a ≤ a * b≤ a * b

          le_self_mul : ∀ (a b : α), a 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
          theorem le_self_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {c : α} :
          a a + c
          theorem le_self_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {c : α} :
          a a * c
          theorem le_add_self {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :
          a b + a
          theorem le_mul_self {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :
          a b * a
          @[simp]
          theorem self_le_add_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) (b : α) :
          a a + b
          @[simp]
          theorem self_le_mul_right {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) (b : α) :
          a a * b
          @[simp]
          theorem self_le_add_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) (b : α) :
          a b + a
          @[simp]
          theorem self_le_mul_left {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) (b : α) :
          a b * a
          theorem le_of_add_le_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} :
          a + b ca c
          theorem le_of_mul_le_left {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} :
          a * b ca c
          theorem le_of_add_le_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} :
          a + b cb c
          theorem le_of_mul_le_right {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} :
          a * b cb c
          theorem le_iff_exists_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :
          a b c, b = a + c
          theorem le_iff_exists_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :
          a b c, b = a * c
          theorem le_iff_exists_add' {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :
          a b c, b = c + a
          theorem le_iff_exists_mul' {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :
          a b c, b = c * a
          @[simp]
          theorem zero_le {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) :
          0 a
          @[simp]
          theorem one_le {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) :
          1 a
          theorem bot_eq_one {α : Type u} [inst : CanonicallyOrderedMonoid α] :
          = 1
          @[simp]
          theorem add_eq_zero_iff {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :
          a + b = 0 a = 0 b = 0
          @[simp]
          theorem mul_eq_one_iff {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :
          a * b = 1 a = 1 b = 1
          @[simp]
          theorem nonpos_iff_eq_zero {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :
          a 0 a = 0
          @[simp]
          theorem le_one_iff_eq_one {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :
          a 1 a = 1
          theorem pos_iff_ne_zero {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :
          0 < a a 0
          theorem one_lt_iff_ne_one {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :
          1 < a a 1
          theorem eq_zero_or_pos {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :
          a = 0 0 < a
          theorem eq_one_or_one_lt {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :
          a = 1 1 < a
          @[simp]
          theorem add_pos_iff {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :
          0 < a + b 0 < a 0 < b
          @[simp]
          theorem one_lt_mul_iff {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :
          1 < a * b 1 < a 1 < b
          theorem exists_pos_add_of_lt {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} (h : a < b) :
          c x, a + c = b
          theorem exists_one_lt_mul_of_lt {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} (h : a < b) :
          c x, a * c = b
          theorem le_add_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} (h : a c) :
          a b + c
          theorem le_mul_left {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} (h : a c) :
          a b * c
          theorem le_add_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} (h : a b) :
          a b + c
          theorem le_mul_right {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} (h : a b) :
          a b * c
          theorem lt_iff_exists_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
          a < b c, c > 0 b = a + c
          theorem lt_iff_exists_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
          a < b c, c > 1 b = a * c
          theorem pos_of_gt {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {n : M} {m : M} (h : n < m) :
          0 < m
          theorem NeZero.pos {M : Type u_1} (a : M) [inst : CanonicallyOrderedAddMonoid M] [inst : NeZero a] :
          0 < a
          theorem NeZero.of_gt {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {x : M} {y : M} (h : x < y) :
          instance NeZero.of_gt' {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] [inst : One M] {y : M} [inst : Fact (1 < y)] :
          Equations
          instance NeZero.bit0 {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {x : M} [inst : NeZero x] :
          Equations
          • A linear order is total.

            le_total : ∀ (a b : α), a b b a
          • In a linearly ordered type, we assume the order relations are all decidable.

            decidable_le : DecidableRel fun x x_1 => x x_1
          • In 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_1
          • The minimum function is equivalent to the one you get from minOfLe.

            min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
          • The minimum function is equivalent to the one you get from maxOfLe.

            max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝

          A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

          Instances
            • A linear order is total.

              le_total : ∀ (a b : α), a b b a
            • In a linearly ordered type, we assume the order relations are all decidable.

              decidable_le : DecidableRel fun x x_1 => x x_1
            • In 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_1
            • The minimum function is equivalent to the one you get from minOfLe.

              min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
            • The minimum function is equivalent to the one you get from maxOfLe.

              max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝

            A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.

            Instances
              Equations
              • (_ : ∀ (a b : α), b a b) = (_ : ∀ (a b : α), b a b)
              Equations
              • One or more equations did not get rendered due to their size.
              def CanonicallyLinearOrderedAddMonoid.semilatticeSup.proof_3 {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :
              a cb ca b c
              Equations
              • (_ : ∀ (a b c : α), a cb ca b c) = (_ : ∀ (a b c : α), a cb ca b c)
              Equations
              • (_ : ∀ (a b : α), a a b) = (_ : ∀ (a b : α), a a b)
              Equations
              • One or more equations did not get rendered due to their size.
              theorem min_add_distrib {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :
              min a (b + c) = min a (min a b + min a c)
              theorem min_mul_distrib {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) (b : α) (c : α) :
              min a (b * c) = min a (min a b * min a c)
              theorem min_add_distrib' {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :
              min (a + b) c = min (min a c + min b c) c
              theorem min_mul_distrib' {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) (b : α) (c : α) :
              min (a * b) c = min (min a c * min b c) c
              theorem zero_min {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) :
              min 0 a = 0
              theorem one_min {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) :
              min 1 a = 1
              theorem min_zero {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) :
              min a 0 = 0
              theorem min_one {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) :
              min a 1 = 1
              @[simp]
              theorem bot_eq_zero' {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] :
              = 0

              In a linearly ordered monoid, we are happy for bot_eq_zero to be a @[simp] lemma

              @[simp]
              theorem bot_eq_one' {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] :
              = 1

              In a linearly ordered monoid, we are happy for bot_eq_one to be a @[simp] lemma.