Ordered cancellative monoids

ink

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

• Addition is monotone in an ordered cancellative additive commutative monoid.

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

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

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

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

ink

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

• Multiplication is monotone in an ordered cancellative commutative monoid.

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

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

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

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

ink

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

Equations

• (_ : ContravariantClass α α (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)

ink

instance OrderedCancelAddCommMonoid.to_contravariantClass_le_left {α : Type u} [inst : 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

ink

instance OrderedCancelCommMonoid.to_contravariantClass_le_left {α : Type u} [inst : 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

ink

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

ink

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

ink

instance OrderedCancelAddCommMonoid.to_contravariantClass_left (M : Type u_1) [inst : 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

ink

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

Equations

• (_ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1)

ink

instance OrderedCancelCommMonoid.to_contravariantClass_left (M : Type u_1) [inst : 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

ink

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

Equations

• (_ : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1)

ink

instance OrderedCancelAddCommMonoid.to_contravariantClass_right (M : Type u_1) [inst : 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

ink

instance OrderedCancelCommMonoid.to_contravariantClass_right (M : Type u_1) [inst : 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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• (_ : ∀ (a : α), a + 0 = a) = (_ : ∀ (a : α), a + 0 = a)

ink

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

Equations

• (_ : ∀ (x : α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : α), AddMonoid.nsmul 0 x = 0)

ink

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

Equations

• (_ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

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

Equations

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

ink

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

Equations

• (_ : ∀ (a b : α), a + b = b + a) = (_ : ∀ (a b : α), a + b = b + a)

ink

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

Equations

• (_ : b = c) = (_ : b = c)

ink

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

Equations

• (_ : ∀ (a : α), 0 + a = a) = (_ : ∀ (a : α), 0 + a = a)

ink

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

Equations

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

ink

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

• 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 linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

ink

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

• 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 linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.