Documentation

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Canonically ordered monoids #

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
    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
      instance AddGroup.existsAddOfLE (α : Type u) [AddGroup α] [LE α] :
      Equations
      • =
      instance Group.existsMulOfLE (α : Type u) [Group α] [LE α] :
      Equations
      • =
      theorem exists_pos_add_of_lt' {α : Type u} [AddZeroClass α] [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ExistsAddOfLE α] {a : α} {b : α} (h : a < b) :
      ∃ (c : α), 0 < c a + c = b
      theorem exists_one_lt_mul_of_lt' {α : Type u} [MulOneClass α] [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ExistsMulOfLE α] {a : α} {b : α} (h : a < b) :
      ∃ (c : α), 1 < c a * c = b
      theorem le_of_forall_pos_le_add {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} :
      a b ∀ (ε : α), 1 < ε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 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.

      • add : ααα
      • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
      • zero : α
      • zero_add : ∀ (a : α), 0 + a = a
      • add_zero : ∀ (a : α), a + 0 = a
      • nsmul : αα
      • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
      • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
      • add_comm : ∀ (a b : α), a + b = b + a
      • le : ααProp
      • lt : ααProp
      • le_refl : ∀ (a : α), a a
      • le_trans : ∀ (a b c : α), a bb ca c
      • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
      • le_antisymm : ∀ (a b : α), a bb aa = b
      • add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
      • bot : α
      • bot_le : ∀ (a : α), a
      • exists_add_of_le : ∀ {a b : α}, a b∃ (c : α), b = a + c

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

      • le_self_add : ∀ (a b : α), a a + b

        For any a and b, a ≤ a + b

      Instances

        A canonically ordered monoid is an ordered commutative monoid in which 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).

        • mul : ααα
        • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
        • one : α
        • one_mul : ∀ (a : α), 1 * a = a
        • mul_one : ∀ (a : α), a * 1 = a
        • npow : αα
        • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
        • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x * Monoid.npow n x
        • mul_comm : ∀ (a b : α), a * b = b * a
        • le : ααProp
        • lt : ααProp
        • le_refl : ∀ (a : α), a a
        • le_trans : ∀ (a b c : α), a bb ca c
        • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
        • le_antisymm : ∀ (a b : α), a bb aa = b
        • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
        • bot : α
        • bot_le : ∀ (a : α), a
        • exists_mul_of_le : ∀ {a b : α}, a b∃ (c : α), b = a * c

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

        • le_self_mul : ∀ (a b : α), a a * b

          For any a and b, a ≤ a * b

        Instances
          theorem le_self_add {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {c : α} :
          a a + c
          theorem le_self_mul {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {c : α} :
          a a * c
          theorem le_add_self {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
          a b + a
          theorem le_mul_self {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
          a b * a
          @[simp]
          theorem self_le_add_right {α : Type u} [CanonicallyOrderedAddCommMonoid α] (a : α) (b : α) :
          a a + b
          @[simp]
          theorem self_le_mul_right {α : Type u} [CanonicallyOrderedCommMonoid α] (a : α) (b : α) :
          a a * b
          @[simp]
          theorem self_le_add_left {α : Type u} [CanonicallyOrderedAddCommMonoid α] (a : α) (b : α) :
          a b + a
          @[simp]
          theorem self_le_mul_left {α : Type u} [CanonicallyOrderedCommMonoid α] (a : α) (b : α) :
          a b * a
          theorem le_of_add_le_left {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} :
          a + b ca c
          theorem le_of_mul_le_left {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} :
          a * b ca c
          theorem le_of_add_le_right {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} :
          a + b cb c
          theorem le_of_mul_le_right {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} :
          a * b cb c
          theorem le_add_of_le_left {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} :
          a ba b + c
          theorem le_mul_of_le_left {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} :
          a ba b * c
          theorem le_add_of_le_right {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} :
          a ca b + c
          theorem le_mul_of_le_right {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} :
          a ca b * c
          theorem le_iff_exists_add {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
          a b ∃ (c : α), b = a + c
          theorem le_iff_exists_mul {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
          a b ∃ (c : α), b = a * c
          theorem le_iff_exists_add' {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
          a b ∃ (c : α), b = c + a
          theorem le_iff_exists_mul' {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
          a b ∃ (c : α), b = c * a
          @[simp]
          theorem zero_le {α : Type u} [CanonicallyOrderedAddCommMonoid α] (a : α) :
          0 a
          @[simp]
          theorem one_le {α : Type u} [CanonicallyOrderedCommMonoid α] (a : α) :
          1 a
          @[simp]
          theorem add_eq_zero_iff {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
          a + b = 0 a = 0 b = 0
          @[simp]
          theorem mul_eq_one_iff {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
          a * b = 1 a = 1 b = 1
          @[simp]
          theorem nonpos_iff_eq_zero {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} :
          a 0 a = 0
          @[simp]
          theorem le_one_iff_eq_one {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} :
          a 1 a = 1
          theorem pos_iff_ne_zero {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} :
          0 < a a 0
          theorem one_lt_iff_ne_one {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} :
          1 < a a 1
          theorem eq_zero_or_pos {α : Type u} [CanonicallyOrderedAddCommMonoid α] (a : α) :
          a = 0 0 < a
          theorem eq_one_or_one_lt {α : Type u} [CanonicallyOrderedCommMonoid α] (a : α) :
          a = 1 1 < a
          @[simp]
          theorem add_pos_iff {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
          0 < a + b 0 < a 0 < b
          @[simp]
          theorem one_lt_mul_iff {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
          1 < a * b 1 < a 1 < b
          theorem exists_pos_add_of_lt {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} (h : a < b) :
          ∃ (c : α), ∃ (x : 0 < c), a + c = b
          theorem exists_one_lt_mul_of_lt {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} (h : a < b) :
          ∃ (c : α), ∃ (x : 1 < c), a * c = b
          theorem le_add_left {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} (h : a c) :
          a b + c
          theorem le_mul_left {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} (h : a c) :
          a b * c
          theorem le_add_right {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} (h : a b) :
          a b + c
          theorem le_mul_right {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} (h : a b) :
          a b * c
          theorem lt_iff_exists_add {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} [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} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} [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} [CanonicallyOrderedAddCommMonoid M] {n : M} {m : M} (h : n < m) :
          0 < m
          theorem NeZero.pos {M : Type u_1} (a : M) [CanonicallyOrderedAddCommMonoid M] [NeZero a] :
          0 < a
          theorem NeZero.of_gt {M : Type u_1} [CanonicallyOrderedAddCommMonoid M] {x : M} {y : M} (h : x < y) :
          instance NeZero.of_gt' {M : Type u_1} [CanonicallyOrderedAddCommMonoid M] [One M] {y : M} [Fact (1 < y)] :
          Equations
          • =
          instance NeZero.bit0 {M : Type u_1} [CanonicallyOrderedAddCommMonoid M] {x : M} [NeZero x] :
          Equations
          • =

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

          • add : ααα
          • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
          • zero : α
          • zero_add : ∀ (a : α), 0 + a = a
          • add_zero : ∀ (a : α), a + 0 = a
          • nsmul : αα
          • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
          • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
          • add_comm : ∀ (a b : α), a + b = b + a
          • le : ααProp
          • lt : ααProp
          • le_refl : ∀ (a : α), a a
          • le_trans : ∀ (a b c : α), a bb ca c
          • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
          • le_antisymm : ∀ (a b : α), a bb aa = b
          • add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
          • bot : α
          • bot_le : ∀ (a : α), a
          • exists_add_of_le : ∀ {a b : α}, a b∃ (c : α), b = a + c
          • le_self_add : ∀ (a b : α), a a + b
          • min : ααα
          • max : ααα
          • compare : ααOrdering
          • le_total : ∀ (a b : α), a b b a

            A linear order is total.

          • decidableLE : DecidableRel fun (x x_1 : α) => x x_1

            In a linearly ordered type, we assume the order relations are all decidable.

          • decidableEq : DecidableEq α

            In a linearly ordered type, we assume the order relations are all decidable.

          • decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

            In a linearly ordered type, we assume the order relations are all decidable.

          • min_def : ∀ (a b : α), min a b = if a b then a else b

            The minimum function is equivalent to the one you get from minOfLe.

          • max_def : ∀ (a b : α), max a b = if a b then b else a

            The minimum function is equivalent to the one you get from maxOfLe.

          • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

            Comparison via compare is equal to the canonical comparison given decidable < and =.

          Instances

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

            • mul : ααα
            • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
            • one : α
            • one_mul : ∀ (a : α), 1 * a = a
            • mul_one : ∀ (a : α), a * 1 = a
            • npow : αα
            • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
            • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x * Monoid.npow n x
            • mul_comm : ∀ (a b : α), a * b = b * a
            • le : ααProp
            • lt : ααProp
            • le_refl : ∀ (a : α), a a
            • le_trans : ∀ (a b c : α), a bb ca c
            • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
            • le_antisymm : ∀ (a b : α), a bb aa = b
            • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
            • bot : α
            • bot_le : ∀ (a : α), a
            • exists_mul_of_le : ∀ {a b : α}, a b∃ (c : α), b = a * c
            • le_self_mul : ∀ (a b : α), a a * b
            • min : ααα
            • max : ααα
            • compare : ααOrdering
            • le_total : ∀ (a b : α), a b b a

              A linear order is total.

            • decidableLE : DecidableRel fun (x x_1 : α) => x x_1

              In a linearly ordered type, we assume the order relations are all decidable.

            • decidableEq : DecidableEq α

              In a linearly ordered type, we assume the order relations are all decidable.

            • decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

              In a linearly ordered type, we assume the order relations are all decidable.

            • min_def : ∀ (a b : α), min a b = if a b then a else b

              The minimum function is equivalent to the one you get from minOfLe.

            • max_def : ∀ (a b : α), max a b = if a b then b else a

              The minimum function is equivalent to the one you get from maxOfLe.

            • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

              Comparison via compare is equal to the canonical comparison given decidable < and =.

            Instances
              Equations
              • CanonicallyLinearOrderedAddCommMonoid.semilatticeSup = let __src := LinearOrder.toLattice; SemilatticeSup.mk
              theorem CanonicallyLinearOrderedAddCommMonoid.semilatticeSup.proof_3 {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) (b : α) (c : α) :
              a cb ca b c
              Equations
              • CanonicallyLinearOrderedCommMonoid.semilatticeSup = let __src := LinearOrder.toLattice; SemilatticeSup.mk
              theorem min_add_distrib {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) (b : α) (c : α) :
              min a (b + c) = min a (min a b + min a c)
              theorem min_mul_distrib {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) (b : α) (c : α) :
              min a (b * c) = min a (min a b * min a c)
              theorem min_add_distrib' {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) (b : α) (c : α) :
              min (a + b) c = min (min a c + min b c) c
              theorem min_mul_distrib' {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) (b : α) (c : α) :
              min (a * b) c = min (min a c * min b c) c
              theorem zero_min {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) :
              min 0 a = 0
              theorem one_min {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) :
              min 1 a = 1
              theorem min_zero {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) :
              min a 0 = 0
              theorem min_one {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) :
              min a 1 = 1
              @[simp]

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

              @[simp]

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