algebra.order.monoid.cancel.defs

@[class]

structure ordered_cancel_add_comm_monoid (α : 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 : α), ordered_cancel_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_cancel_add_comm_monoid.nsmul n.succ x = x + ordered_cancel_add_comm_monoid.nsmul n x) . "try_refl_tac"
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) . "order_laws_tac"
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

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

Instances of this typeclass

Instances of other typeclasses for ordered_cancel_add_comm_monoid

ordered_cancel_add_comm_monoid.has_sizeof_inst

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_comm_monoid (α : Type u) [self : ordered_cancel_add_comm_monoid α] :

add_comm_monoid α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_partial_order (α : Type u) [self : ordered_cancel_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_partial_order (α : Type u) [self : ordered_cancel_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_comm_monoid (α : Type u) [self : ordered_cancel_comm_monoid α] :

comm_monoid α

source

@[class]

structure ordered_cancel_comm_monoid (α : Type u) :

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 : α), ordered_cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), ordered_cancel_comm_monoid.npow n.succ x = x * ordered_cancel_comm_monoid.npow n x) . "try_refl_tac"
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) . "order_laws_tac"
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

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

Instances of this typeclass

Instances of other typeclasses for ordered_cancel_comm_monoid

ordered_cancel_comm_monoid.has_sizeof_inst

source

@[protected, instance]

def ordered_cancel_add_comm_monoid.to_contravariant_class_le_left {α : Type u} [ordered_cancel_add_comm_monoid α] :

contravariant_class α α has_add.add has_le.le

source

@[protected, instance]

def ordered_cancel_comm_monoid.to_contravariant_class_le_left {α : Type u} [ordered_cancel_comm_monoid α] :

contravariant_class α α has_mul.mul has_le.le

source

theorem ordered_cancel_add_comm_monoid.lt_of_add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a b c : α) :

a + b < a + c → b < c

source

theorem ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left {α : Type u} [ordered_cancel_comm_monoid α] (a b c : α) :

a * b < a * c → b < c

source

@[protected, instance]

def ordered_cancel_comm_monoid.to_contravariant_class_left (M : Type u_1) [ordered_cancel_comm_monoid M] :

contravariant_class M M has_mul.mul has_lt.lt

source

@[protected, instance]

def ordered_cancel_add_comm_monoid.to_contravariant_class_left (M : Type u_1) [ordered_cancel_add_comm_monoid M] :

contravariant_class M M has_add.add has_lt.lt

source

@[protected, instance]

def ordered_cancel_comm_monoid.to_contravariant_class_right (M : Type u_1) [ordered_cancel_comm_monoid M] :

contravariant_class M M (function.swap has_mul.mul) has_lt.lt

source

@[protected, instance]

def ordered_cancel_add_comm_monoid.to_contravariant_class_right (M : Type u_1) [ordered_cancel_add_comm_monoid M] :

contravariant_class M M (function.swap has_add.add) has_lt.lt

source

@[protected, instance]

def ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

ordered_add_comm_monoid α

Equations

ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid = {add := ordered_cancel_add_comm_monoid.add _inst_1, add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero _inst_1, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le _inst_1, lt := ordered_cancel_add_comm_monoid.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

source

@[protected, instance]

def ordered_cancel_comm_monoid.to_ordered_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

ordered_comm_monoid α

Equations

ordered_cancel_comm_monoid.to_ordered_comm_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_cancel_comm_monoid.le _inst_1, lt := ordered_cancel_comm_monoid.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

@[protected, instance]

def ordered_cancel_comm_monoid.to_cancel_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

cancel_comm_monoid α

Equations

ordered_cancel_comm_monoid.to_cancel_comm_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def ordered_cancel_add_comm_monoid.to_cancel_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

add_cancel_comm_monoid α

Equations

ordered_cancel_add_comm_monoid.to_cancel_add_comm_monoid = {add := ordered_cancel_add_comm_monoid.add _inst_1, add_assoc := _, add_left_cancel := _, zero := ordered_cancel_add_comm_monoid.zero _inst_1, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[class]

structure linear_ordered_cancel_add_comm_monoid (α : Type u) :

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 : α), linear_ordered_cancel_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_cancel_add_comm_monoid.nsmul n.succ x = x + linear_ordered_cancel_add_comm_monoid.nsmul n x) . "try_refl_tac"
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) . "order_laws_tac"
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
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
max : α → α → α
max_def : linear_ordered_cancel_add_comm_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_cancel_add_comm_monoid.min = min_default . "reflexivity"

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 of this typeclass

Instances of other typeclasses for linear_ordered_cancel_add_comm_monoid

linear_ordered_cancel_add_comm_monoid.has_sizeof_inst

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid (α : Type u) [self : linear_ordered_cancel_add_comm_monoid α] :

ordered_cancel_add_comm_monoid α

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_linear_ordered_add_comm_monoid (α : Type u) [self : linear_ordered_cancel_add_comm_monoid α] :

linear_ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_cancel_comm_monoid.to_linear_ordered_comm_monoid (α : Type u) [self : linear_ordered_cancel_comm_monoid α] :

linear_ordered_comm_monoid α

source

@[instance]

def linear_ordered_cancel_comm_monoid.to_ordered_cancel_comm_monoid (α : Type u) [self : linear_ordered_cancel_comm_monoid α] :

ordered_cancel_comm_monoid α

source

@[class]

structure linear_ordered_cancel_comm_monoid (α : Type u) :

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 : α), linear_ordered_cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_cancel_comm_monoid.npow n.succ x = x * linear_ordered_cancel_comm_monoid.npow n x) . "try_refl_tac"
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) . "order_laws_tac"
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
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
max : α → α → α
max_def : linear_ordered_cancel_comm_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_cancel_comm_monoid.min = min_default . "reflexivity"

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

Instances of this typeclass

Instances of other typeclasses for linear_ordered_cancel_comm_monoid

linear_ordered_cancel_comm_monoid.has_sizeof_inst

mathlib3 documentation

Ordered cancellative monoids #