Ordered cancellative monoids

class OrderedCancelAddCommMonoid (α : Type u) extends AddCommMonoid , PartialOrder : Type u

• 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

  Addition is monotone in an ordered cancellative additive commutative monoid.

• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c

  Additive cancellation is compatible with the order in an ordered cancellative additive commutative monoid.

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

class OrderedCancelCommMonoid (α : Type u) extends CommMonoid , PartialOrder : Type u

• 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b

  Multiplication is monotone in an ordered cancellative commutative monoid.

• le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c

  Cancellation is compatible with the order in an ordered cancellative commutative monoid.

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and monotone.

theorem OrderedCancelAddCommMonoid.to_contravariantClass_le_left.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance OrderedCancelAddCommMonoid.to_contravariantClass_le_left {α : Type u} [OrderedCancelAddCommMonoid α] : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @OrderedCancelAddCommMonoid.to_contravariantClass_le_left = @OrderedCancelAddCommMonoid.to_contravariantClass_le_left.proof_1

instance OrderedCancelCommMonoid.to_contravariantClass_le_left {α : Type u} [OrderedCancelCommMonoid α] : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• @OrderedCancelCommMonoid.to_contravariantClass_le_left = @OrderedCancelCommMonoid.to_contravariantClass_le_left.proof_1

theorem OrderedCancelAddCommMonoid.lt_of_add_lt_add_left {α : Type u} [OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) : a + b < a + c → b < c

theorem OrderedCancelCommMonoid.lt_of_mul_lt_mul_left {α : Type u} [OrderedCancelCommMonoid α] (a : α) (b : α) (c : α) : a * b < a * c → b < c

instance OrderedCancelAddCommMonoid.to_contravariantClass_left (M : Type u_1) [OrderedCancelAddCommMonoid M] : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• OrderedCancelAddCommMonoid.to_contravariantClass_left = OrderedCancelAddCommMonoid.to_contravariantClass_left.proof_1

theorem OrderedCancelAddCommMonoid.to_contravariantClass_left.proof_1 (M : Type u_1) [OrderedCancelAddCommMonoid M] : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1

instance OrderedCancelCommMonoid.to_contravariantClass_left (M : Type u_1) [OrderedCancelCommMonoid M] : ContravariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

• OrderedCancelCommMonoid.to_contravariantClass_left = OrderedCancelCommMonoid.to_contravariantClass_left.proof_1

theorem OrderedCancelAddCommMonoid.to_contravariantClass_right.proof_1 (M : Type u_1) [OrderedCancelAddCommMonoid M] : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

instance OrderedCancelAddCommMonoid.to_contravariantClass_right (M : Type u_1) [OrderedCancelAddCommMonoid M] : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• OrderedCancelAddCommMonoid.to_contravariantClass_right = OrderedCancelAddCommMonoid.to_contravariantClass_right.proof_1

instance OrderedCancelCommMonoid.to_contravariantClass_right (M : Type u_1) [OrderedCancelCommMonoid M] : ContravariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

• OrderedCancelCommMonoid.to_contravariantClass_right = OrderedCancelCommMonoid.to_contravariantClass_right.proof_1

instance OrderedCancelAddCommMonoid.toOrderedAddCommMonoid {α : Type u} [OrderedCancelAddCommMonoid α] : OrderedAddCommMonoid α

Equations

• OrderedCancelAddCommMonoid.toOrderedAddCommMonoid = let src := inst; OrderedAddCommMonoid.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

instance OrderedCancelCommMonoid.toOrderedCommMonoid {α : Type u} [OrderedCancelCommMonoid α] : OrderedCommMonoid α

Equations

• OrderedCancelCommMonoid.toOrderedCommMonoid = let src := inst; OrderedCommMonoid.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b)

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_3 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) : a + 0 = a

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_4 {α : Type u_1} [OrderedCancelAddCommMonoid α] (x : α) : AddMonoid.nsmul 0 x = 0

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_5 {α : Type u_1} [OrderedCancelAddCommMonoid α] (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

instance OrderedCancelAddCommMonoid.toCancelAddCommMonoid {α : Type u} [OrderedCancelAddCommMonoid α] : AddCancelCommMonoid α

Equations

• OrderedCancelAddCommMonoid.toCancelAddCommMonoid = let src := inst; AddCancelCommMonoid.mk (_ : ∀ (a b : α), a + b = b + a)

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_6 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) : a + b = b + a

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) (h : a + b = a + c) : b = c

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) : 0 + a = a

instance OrderedCancelCommMonoid.toCancelCommMonoid {α : Type u} [OrderedCancelCommMonoid α] : CancelCommMonoid α

Equations

• OrderedCancelCommMonoid.toCancelCommMonoid = let src := inst; CancelCommMonoid.mk (_ : ∀ (a b : α), a * b = b * a)

class LinearOrderedCancelAddCommMonoid (α : Type u) extends OrderedCancelAddCommMonoid , Min , Max , Ord : Type u

• 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
• 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 =.

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

class LinearOrderedCancelCommMonoid (α : Type u) extends OrderedCancelCommMonoid , Min , Max , Ord : Type u

• 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
• le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
• 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 =.

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.