Documentation

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Canonically ordered monoids #

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 = AddMonoid.nsmul n x + 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
    theorem CanonicallyOrderedAddCommMonoid.exists_add_of_le {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} :
    a b∃ (c : α), b = a + c

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

    theorem CanonicallyOrderedAddCommMonoid.le_self_add {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] (a : α) (b : α) :
    a a + b

    For any a and 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 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 = Monoid.npow n x * 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 CanonicallyOrderedCommMonoid.exists_mul_of_le {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] {a : α} {b : α} :
      a b∃ (c : α), b = a * c

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

      theorem CanonicallyOrderedCommMonoid.le_self_mul {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] (a : α) (b : α) :
      a a * b

      For any a and b, a ≤ a * b

      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =
      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 10]
      instance NeZero.of_gt' {M : Type u_1} [CanonicallyOrderedAddCommMonoid M] [One M] {y : M} [Fact (1 < y)] :
      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 = AddMonoid.nsmul n x + 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 = Monoid.npow n x * 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
          @[instance 100]
          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
          @[instance 100]
          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.