# Documentation

Mathlib.Algebra.Order.Monoid.Cancel.Defs

# Ordered cancellative monoids #

class OrderedCancelAddCommMonoid (α : Type u) extends , :

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 + cb c

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

Instances
class OrderedCancelCommMonoid (α : Type u) extends , :
• 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 * cb c

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

Instances
def OrderedCancelAddCommMonoid.to_contravariantClass_le_left.proof_1 {α : Type u_1} [inst : ] :
ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderedCancelAddCommMonoid.to_contravariantClass_le_left {α : Type u} [inst : ] :
ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderedCancelCommMonoid.to_contravariantClass_le_left {α : Type u} [inst : ] :
ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
theorem OrderedCancelAddCommMonoid.lt_of_add_lt_add_left {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a + b < a + cb < c
theorem OrderedCancelCommMonoid.lt_of_mul_lt_mul_left {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a * b < a * cb < c
instance OrderedCancelAddCommMonoid.to_contravariantClass_left (M : Type u_1) [inst : ] :
ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
def OrderedCancelAddCommMonoid.to_contravariantClass_left.proof_1 (M : Type u_1) [inst : ] :
ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderedCancelCommMonoid.to_contravariantClass_left (M : Type u_1) [inst : ] :
ContravariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
def OrderedCancelAddCommMonoid.to_contravariantClass_right.proof_1 (M : Type u_1) [inst : ] :
ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderedCancelAddCommMonoid.to_contravariantClass_right (M : Type u_1) [inst : ] :
ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderedCancelCommMonoid.to_contravariantClass_right (M : Type u_1) [inst : ] :
ContravariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
Equations
Equations
• OrderedCancelCommMonoid.toOrderedCommMonoid = let src := inst; OrderedCommMonoid.mk (_ : ∀ (a b : α), a b∀ (c : α), c * a c * b)
def OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_3 {α : Type u_1} [inst : ] (a : α) :
a + 0 = a
Equations
• (_ : ∀ (a : α), a + 0 = a) = (_ : ∀ (a : α), a + 0 = a)
Equations
• (_ : ∀ (x : α), = 0) = (_ : ∀ (x : α), = 0)
def OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_5 {α : Type u_1} [inst : ] (n : ) (x : α) :
AddMonoid.nsmul (n + 1) x = x +
Equations
Equations
def OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_6 {α : Type u_1} [inst : ] (a : α) (b : α) :
a + b = b + a
Equations
• (_ : ∀ (a b : α), a + b = b + a) = (_ : ∀ (a b : α), a + b = b + a)
def OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : α) (b : α) (c : α) (h : a + b = a + c) :
b = c
Equations
• (_ : b = c) = (_ : b = c)
def OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : α) :
0 + a = a
Equations
• (_ : ∀ (a : α), 0 + a = a) = (_ : ∀ (a : α), 0 + a = a)
instance OrderedCancelCommMonoid.toCancelCommMonoid {α : Type u} [inst : ] :
Equations
• OrderedCancelCommMonoid.toCancelCommMonoid = let src := inst; CancelCommMonoid.mk (_ : ∀ (a b : α), a * b = b * a)
class LinearOrderedCancelAddCommMonoid (α : Type u) extends , , :
• 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 :
• 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.

Instances
class LinearOrderedCancelCommMonoid (α : Type u) extends , , :
• 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 :
• 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.

Instances