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

For a ≤ b, a left divides b

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 : ] {a : α} {b : α} :
a b∃ (c : α), b = a + c

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

@[instance 100]
Equations
• =
@[instance 100]
instance Group.existsMulOfLE (α : Type u) [] [LE α] :
Equations
• =
theorem exists_pos_add_of_lt' {α : Type u} [] [] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [] {a : α} {b : α} (h : a < b) :
∃ (c : α), 0 < c a + c = b
theorem exists_one_lt_mul_of_lt' {α : Type u} [] [] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [] {a : α} {b : α} (h : a < b) :
∃ (c : α), 1 < c a * c = b
theorem le_of_forall_pos_le_add {α : Type u} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [] [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 * ε
class CanonicallyOrderedAddCommMonoid (α : Type u_1) extends , :
Type u_1

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_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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) 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 : ] {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 : ] (a : α) (b : α) :
a a + b

For any a and b, a ≤ a + b

class CanonicallyOrderedCommMonoid (α : Type u_1) extends , :
Type u_1

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

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

• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) 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 :

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 =

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

Instances
class CanonicallyLinearOrderedCommMonoid (α : Type u_1) extends , , , :
Type u_1

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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) 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 :

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 =

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

Instances
@[instance 100]
Equations
• CanonicallyLinearOrderedAddCommMonoid.semilatticeSup = let __src := LinearOrder.toLattice;
theorem CanonicallyLinearOrderedAddCommMonoid.semilatticeSup.proof_3 {α : Type u_1} (a : α) (b : α) (c : α) :
a cb ca b c
@[instance 100]
Equations
• CanonicallyLinearOrderedCommMonoid.semilatticeSup = let __src := LinearOrder.toLattice;
theorem min_add_distrib {α : Type u} (a : α) (b : α) (c : α) :
min a (b + c) = min a (min a b + min a c)
theorem min_mul_distrib {α : Type u} (a : α) (b : α) (c : α) :
min a (b * c) = min a (min a b * min a c)
theorem min_add_distrib' {α : Type u} (a : α) (b : α) (c : α) :
min (a + b) c = min (min a c + min b c) c
theorem min_mul_distrib' {α : Type u} (a : α) (b : α) (c : α) :
min (a * b) c = min (min a c * min b c) c
theorem zero_min {α : Type u} (a : α) :
min 0 a = 0
theorem one_min {α : Type u} (a : α) :
min 1 a = 1
theorem min_zero {α : Type u} (a : α) :
min a 0 = 0
theorem min_one {α : Type u} (a : α) :
min a 1 = 1
@[simp]
theorem bot_eq_zero' {α : Type u} :
= 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} :
= 1

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