algebra.ordered_monoid - mathlib docs

source

@[instance]

def ordered_comm_monoid.to_comm_monoid (α : Type u_1) [self : ordered_comm_monoid α] :

comm_monoid α

source

@[instance]

def ordered_comm_monoid.to_partial_order (α : Type u_1) [self : ordered_comm_monoid α] :

partial_order α

source

@[class]

structure ordered_comm_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), ordered_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_monoid.npow n.succ x = x * ordered_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

An ordered commutative monoid is a commutative monoid with a partial order such that

a ≤ b → c * a ≤ c * b (multiplication is monotone)
a * b < a * c → b < c.

Instances

source

@[instance]

def ordered_add_comm_monoid.to_partial_order (α : Type u_1) [self : ordered_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_add_comm_monoid.to_add_comm_monoid (α : Type u_1) [self : ordered_add_comm_monoid α] :

add_comm_monoid α

source

@[class]

structure ordered_add_comm_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), ordered_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_add_comm_monoid.nsmul n.succ x = x + ordered_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that

a ≤ b → c + a ≤ c + b (addition is monotone)
a + b < a + c → b < c.

Instances

source

@[instance]

def ordered_add_comm_monoid.to_covariant_class_left (M : Type u_1) [ordered_add_comm_monoid M] :

covariant_class M M has_add.add has_le.le

source

@[instance]

def ordered_comm_monoid.to_covariant_class_left (M : Type u_1) [ordered_comm_monoid M] :

covariant_class M M has_mul.mul has_le.le

source

@[instance]

def ordered_comm_monoid.to_covariant_class_right (M : Type u_1) [ordered_comm_monoid M] :

covariant_class M M (function.swap has_mul.mul) has_le.le

source

@[instance]

def ordered_add_comm_monoid.to_covariant_class_right (M : Type u_1) [ordered_add_comm_monoid M] :

covariant_class M M (function.swap has_add.add) has_le.le

source

@[instance]

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

contravariant_class M M has_add.add has_lt.lt

source

@[instance]

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

contravariant_class M M has_mul.mul has_lt.lt

source

@[instance]

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

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

source

@[instance]

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

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

source

@[class]

structure has_exists_mul_of_le (α : Type u) [ordered_comm_monoid α] :

Prop

exists_mul_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a * c)

An ordered_comm_monoid 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 canonically_ordered_monoid.

Instances

source

@[class]

structure has_exists_add_of_le (α : Type u) [ordered_add_comm_monoid α] :

Prop

exists_add_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a + c)

An ordered_add_comm_monoid 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 canonically_ordered_add_monoid.

Instances

source

@[instance]

def linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid (α : Type u_1) [self : linear_ordered_add_comm_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid.to_linear_order (α : Type u_1) [self : linear_ordered_add_comm_monoid α] :

linear_order α

source

@[class]

structure linear_ordered_add_comm_monoid (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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
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
add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), linear_ordered_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_add_comm_monoid.nsmul n.succ x = x + linear_ordered_add_comm_monoid.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

A linearly ordered additive commutative monoid.

Instances

source

@[class]

structure linear_ordered_comm_monoid (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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
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
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), linear_ordered_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_monoid.npow n.succ x = x * linear_ordered_comm_monoid.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

A linearly ordered commutative monoid.

Instances

source

@[instance]

def linear_ordered_comm_monoid.to_linear_order (α : Type u_1) [self : linear_ordered_comm_monoid α] :

linear_order α

source

@[instance]

def linear_ordered_comm_monoid.to_ordered_comm_monoid (α : Type u_1) [self : linear_ordered_comm_monoid α] :

ordered_comm_monoid α

source

@[instance]

def linear_ordered_comm_monoid_with_zero.to_comm_monoid_with_zero (α : Type u_1) [self : linear_ordered_comm_monoid_with_zero α] :

comm_monoid_with_zero α

source

@[class]

structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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
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
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), linear_ordered_comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_monoid_with_zero.npow n.succ x = x * linear_ordered_comm_monoid_with_zero.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
zero : α
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
zero_le_one : 0 ≤ 1

A linearly ordered commutative monoid with a zero element.

Instances

source

@[instance]

def linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid (α : Type u_1) [self : linear_ordered_comm_monoid_with_zero α] :

linear_ordered_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid_with_top.to_linear_ordered_add_comm_monoid (α : Type u_1) [self : linear_ordered_add_comm_monoid_with_top α] :

linear_ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid_with_top.to_order_top (α : Type u_1) [self : linear_ordered_add_comm_monoid_with_top α] :

order_top α

source

@[class]

structure linear_ordered_add_comm_monoid_with_top (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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
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
add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), linear_ordered_add_comm_monoid_with_top.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_add_comm_monoid_with_top.nsmul n.succ x = x + linear_ordered_add_comm_monoid_with_top.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
top : α
le_top : ∀ (a : α), a ≤ ⊤
top_add' : ∀ (x : α), ⊤ + x = ⊤

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.`

Instances

source

@[simp]

theorem top_add {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :

⊤ + a = ⊤

source

@[simp]

theorem add_top {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :

a + ⊤ = ⊤

source

def function.injective.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

ordered_comm_monoid β

Pullback an ordered_comm_monoid under an injective map. See note [reducible non-instances].

Equations

function.injective.ordered_comm_monoid f hf one mul = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def function.injective.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

source

def function.injective.linear_ordered_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

linear_ordered_comm_monoid β

Pullback a linear_ordered_comm_monoid under an injective map. See note [reducible non-instances].

Equations

function.injective.linear_ordered_comm_monoid f hf one mul = {le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def function.injective.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

linear_ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

source

theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} (h : 0 < a) :

0 < bit0 a

source

@[instance]

def add_units.preorder {α : Type u} [add_monoid α] [preorder α] :

preorder (add_units α)

source

@[instance]

def units.preorder {α : Type u} [monoid α] [preorder α] :

preorder (units α)

Equations

units.preorder = preorder.lift coe

source

@[simp]

theorem add_units.coe_le_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem add_units.coe_lt_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :

↑a < ↑b ↔ a < b

source

@[simp]

theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :

↑a < ↑b ↔ a < b

source

@[instance]

def add_units.partial_order {α : Type u} [add_monoid α] [partial_order α] :

partial_order (add_units α)

source

@[instance]

def units.partial_order {α : Type u} [monoid α] [partial_order α] :

partial_order (units α)

Equations

units.partial_order = partial_order.lift coe units.ext

source

@[instance]

def units.linear_order {α : Type u} [monoid α] [linear_order α] :

linear_order (units α)

Equations

units.linear_order = linear_order.lift coe units.ext

source

@[instance]

def add_units.linear_order {α : Type u} [add_monoid α] [linear_order α] :

linear_order (add_units α)

source

@[simp]

theorem add_units.max_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :

↑(max a b) = max ↑a ↑b

source

@[simp]

theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :

↑(max a b) = max ↑a ↑b

source

@[simp]

theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :

↑(min a b) = min ↑a ↑b

source

@[simp]

theorem add_units.min_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :

↑(min a b) = min ↑a ↑b

source

@[instance]

def with_zero.preorder {α : Type u} [preorder α] :

preorder (with_zero α)

Equations

with_zero.preorder = with_bot.preorder

source

@[instance]

def with_zero.partial_order {α : Type u} [partial_order α] :

partial_order (with_zero α)

Equations

with_zero.partial_order = with_bot.partial_order

source

@[instance]

def with_zero.order_bot {α : Type u} [partial_order α] :

order_bot (with_zero α)

Equations

with_zero.order_bot = with_bot.order_bot

source

theorem with_zero.zero_le {α : Type u} [partial_order α] (a : with_zero α) :

0 ≤ a

source

theorem with_zero.zero_lt_coe {α : Type u} [preorder α] (a : α) :

0 < ↑a

source

@[simp]

theorem with_zero.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :

↑a < ↑b ↔ a < b

source

@[simp]

theorem with_zero.coe_le_coe {α : Type u} [partial_order α] {a b : α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[instance]

def with_zero.lattice {α : Type u} [lattice α] :

lattice (with_zero α)

Equations

with_zero.lattice = with_bot.lattice

source

@[instance]

def with_zero.linear_order {α : Type u} [linear_order α] :

linear_order (with_zero α)

Equations

with_zero.linear_order = with_bot.linear_order

source

theorem with_zero.mul_le_mul_left {α : Type u} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] (a b : with_zero α) :

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

source

theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} [has_mul α] [partial_order α] [contravariant_class α α has_mul.mul has_lt.lt] (a b c : with_zero α) :

a * b < a * c → b < c

source

@[instance]

def with_zero.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] :

ordered_comm_monoid (with_zero α)

Equations

with_zero.ordered_comm_monoid = {mul := comm_monoid_with_zero.mul with_zero.comm_monoid_with_zero, mul_assoc := _, one := comm_monoid_with_zero.one with_zero.comm_monoid_with_zero, one_mul := _, mul_one := _, npow := comm_monoid_with_zero.npow with_zero.comm_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def with_zero.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] (zero_le : ∀ (a : α), 0 ≤ a) :

ordered_add_comm_monoid (with_zero α)

If 0 is the least element in α, then with_zero α is an ordered_add_comm_monoid.

Equations

with_zero.ordered_add_comm_monoid zero_le = {add := add_comm_monoid.add with_zero.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_zero.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_zero.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

@[instance]

def with_top.has_one {α : Type u} [has_one α] :

has_one (with_top α)

Equations

with_top.has_one = {one := ↑1}

source

@[instance]

def with_top.has_zero {α : Type u} [has_zero α] :

has_zero (with_top α)

source

@[simp]

theorem with_top.coe_one {α : Type u} [has_one α] :

↑1 = 1

source

@[simp]

theorem with_top.coe_zero {α : Type u} [has_zero α] :

↑0 = 0

source

@[simp]

theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :

↑a = 0 ↔ a = 0

source

@[simp]

theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :

↑a = 1 ↔ a = 1

source

@[simp]

theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :

0 = ↑a ↔ a = 0

source

@[simp]

theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :

1 = ↑a ↔ a = 1

source

@[simp]

theorem with_top.top_ne_one {α : Type u} [has_one α] :

⊤ ≠ 1

source

@[simp]

theorem with_top.top_ne_zero {α : Type u} [has_zero α] :

⊤ ≠ 0

source

@[simp]

theorem with_top.zero_ne_top {α : Type u} [has_zero α] :

0 ≠ ⊤

source

@[simp]

theorem with_top.one_ne_top {α : Type u} [has_one α] :

1 ≠ ⊤

source

@[instance]

def with_top.has_add {α : Type u} [has_add α] :

has_add (with_top α)

Equations

with_top.has_add = {add := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a + b) o₂)}

source

@[instance]

def with_top.add_semigroup {α : Type u} [add_semigroup α] :

add_semigroup (with_top α)

Equations

with_top.add_semigroup = {add := has_add.add with_top.has_add, add_assoc := _}

source

theorem with_top.coe_add {α : Type u} [has_add α] {a b : α} :

↑(a + b) = ↑a + ↑b

source

theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :

↑(bit0 a) = bit0 ↑a

source

theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem with_top.add_top {α : Type u} [has_add α] {a : with_top α} :

a + ⊤ = ⊤

source

@[simp]

theorem with_top.top_add {α : Type u} [has_add α] {a : with_top α} :

⊤ + a = ⊤

source

theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

source

theorem with_top.add_lt_top {α : Type u} [has_add α] [partial_order α] {a b : with_top α} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

source

theorem with_top.add_eq_coe {α : Type u} [has_add α] {a b : with_top α} {c : α} :

a + b = ↑c ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c

source

@[instance]

def with_top.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :

add_comm_semigroup (with_top α)

Equations

with_top.add_comm_semigroup = {add := add_comm_semigroup.add additive.add_comm_semigroup, add_assoc := _, add_comm := _}

source

@[instance]

def with_top.add_monoid {α : Type u} [add_monoid α] :

add_monoid (with_top α)

Equations

with_top.add_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := some 0, zero_add := _, add_zero := _, nsmul := nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _}

source

@[instance]

def with_top.add_comm_monoid {α : Type u} [add_comm_monoid α] :

add_comm_monoid (with_top α)

Equations

with_top.add_comm_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul additive.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[instance]

def with_top.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :

ordered_add_comm_monoid (with_top α)

Equations

with_top.ordered_add_comm_monoid = {add := add_comm_monoid.add with_top.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_top.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_top.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

@[instance]

def with_top.linear_ordered_add_comm_monoid_with_top {α : Type u} [linear_ordered_add_comm_monoid α] :

linear_ordered_add_comm_monoid_with_top (with_top α)

Equations

with_top.linear_ordered_add_comm_monoid_with_top = {le := order_top.le with_top.order_top, lt := order_top.lt with_top.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le with_top.linear_order, decidable_eq := linear_order.decidable_eq with_top.linear_order, decidable_lt := linear_order.decidable_lt with_top.linear_order, add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul with_top.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, top := order_top.top with_top.order_top, le_top := _, top_add' := _}

source

def with_top.coe_add_hom {α : Type u} [add_monoid α] :

α →+ with_top α

Coercion from α to with_top α as an add_monoid_hom.

Equations

with_top.coe_add_hom = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

theorem with_top.coe_coe_add_hom {α : Type u} [add_monoid α] :

⇑with_top.coe_add_hom = coe

source

@[simp]

theorem with_top.zero_lt_top {α : Type u} [ordered_add_comm_monoid α] :

0 < ⊤

source

@[simp]

theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :

0 < ↑a ↔ 0 < a

source

@[instance]

def with_bot.has_zero {α : Type u} [has_zero α] :

has_zero (with_bot α)

Equations

with_bot.has_zero = with_top.has_zero

source

@[instance]

def with_bot.has_one {α : Type u} [has_one α] :

has_one (with_bot α)

Equations

with_bot.has_one = with_top.has_one

source

@[instance]

def with_bot.add_semigroup {α : Type u} [add_semigroup α] :

add_semigroup (with_bot α)

Equations

with_bot.add_semigroup = with_top.add_semigroup

source

@[instance]

def with_bot.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :

add_comm_semigroup (with_bot α)

Equations

with_bot.add_comm_semigroup = with_top.add_comm_semigroup

source

@[instance]

def with_bot.add_monoid {α : Type u} [add_monoid α] :

add_monoid (with_bot α)

Equations

with_bot.add_monoid = with_top.add_monoid

source

@[instance]

def with_bot.add_comm_monoid {α : Type u} [add_comm_monoid α] :

add_comm_monoid (with_bot α)

Equations

with_bot.add_comm_monoid = with_top.add_comm_monoid

source

@[instance]

def with_bot.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :

ordered_add_comm_monoid (with_bot α)

Equations

with_bot.ordered_add_comm_monoid = {add := add_comm_monoid.add with_bot.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_bot.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_bot.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

@[instance]

def with_bot.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] :

linear_ordered_add_comm_monoid (with_bot α)

Equations

source

theorem with_bot.coe_zero {α : Type u} [has_zero α] :

↑0 = 0

source

theorem with_bot.coe_one {α : Type u} [has_one α] :

↑1 = 1

source

theorem with_bot.coe_eq_zero {α : Type u_1} [add_monoid α] {a : α} :

↑a = 0 ↔ a = 0

source

theorem with_bot.coe_add {α : Type u} [add_semigroup α] (a b : α) :

↑(a + b) = ↑a + ↑b

source

theorem with_bot.coe_bit0 {α : Type u} [add_semigroup α] {a : α} :

↑(bit0 a) = bit0 ↑a

source

theorem with_bot.coe_bit1 {α : Type u} [add_semigroup α] [has_one α] {a : α} :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem with_bot.bot_add {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :

⊥ + a = ⊥

source

@[simp]

theorem with_bot.add_bot {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :

a + ⊥ = ⊥

source

@[instance]

def canonically_ordered_add_monoid.to_ordered_add_comm_monoid (α : Type u_1) [self : canonically_ordered_add_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def canonically_ordered_add_monoid.to_order_bot (α : Type u_1) [self : canonically_ordered_add_monoid α] :

order_bot α

source

@[class]

structure canonically_ordered_add_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), canonically_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_add_monoid.nsmul n.succ x = x + canonically_ordered_add_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_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 ordered_add_comm_groups.

Instances

source

@[instance]

def canonically_ordered_monoid.to_order_bot (α : Type u_1) [self : canonically_ordered_monoid α] :

order_bot α

source

@[instance]

def canonically_ordered_monoid.to_ordered_comm_monoid (α : Type u_1) [self : canonically_ordered_monoid α] :

ordered_comm_monoid α

source

@[class]

structure canonically_ordered_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), canonically_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_monoid.npow n.succ x = x * canonically_ordered_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * c_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. Example seem rare; it seems more likely that the order_dual 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).

Instances

canonically_linear_ordered_monoid.to_canonically_ordered_monoid

source

theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a + c

source

theorem le_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a * c

source

theorem self_le_mul_right {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ a * b

source

theorem self_le_add_right {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ a + b

source

theorem self_le_add_left {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ b + a

source

theorem self_le_mul_left {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ b * a

source

@[simp]

theorem one_le {α : Type u} [canonically_ordered_monoid α] (a : α) :

1 ≤ a

source

@[simp]

theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :

0 ≤ a

source

@[simp]

theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :

⊥ = 1

source

@[simp]

theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :

⊥ = 0

source

@[simp]

theorem mul_eq_one_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a * b = 1 ↔ a = 1 ∧ b = 1

source

@[simp]

theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a + b = 0 ↔ a = 0 ∧ b = 0

source

@[simp]

theorem le_one_iff_eq_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

a ≤ 1 ↔ a = 1

source

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

a ≤ 0 ↔ a = 0

source

theorem one_lt_iff_ne_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

1 < a ↔ a ≠ 1

source

theorem pos_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

0 < a ↔ a ≠ 0

source

theorem exists_pos_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 1), a * c = b

source

theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 0), a + c = b

source

theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b + c

source

theorem le_mul_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b * c

source

theorem le_mul_self {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a ≤ b * a

source

theorem le_add_self {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a ≤ b + a

source

theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b + c

source

theorem le_mul_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b * c

source

theorem le_self_mul {α : Type u} [canonically_ordered_monoid α] {a c : α} :

a ≤ a * c

source

theorem le_self_add {α : Type u} [canonically_ordered_add_monoid α] {a c : α} :

a ≤ a + c

source

@[instance]

def with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_zero α)

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations

with_zero.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add (with_zero.ordered_add_comm_monoid zero_le), add_assoc := _, zero := ordered_add_comm_monoid.zero (with_zero.ordered_add_comm_monoid zero_le), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (with_zero.ordered_add_comm_monoid zero_le), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le (with_zero.ordered_add_comm_monoid zero_le), lt := ordered_add_comm_monoid.lt (with_zero.ordered_add_comm_monoid zero_le), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := 0, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_top α)

Equations

with_top.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul with_top.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := order_bot.le with_top.order_bot, lt := order_bot.lt with_top.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := order_bot.bot with_top.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def canonically_ordered_monoid.has_exists_mul_of_le (α : Type u) [canonically_ordered_monoid α] :

has_exists_mul_of_le α

source

@[instance]

def canonically_ordered_add_monoid.has_exists_add_of_le (α : Type u) [canonically_ordered_add_monoid α] :

has_exists_add_of_le α

source

theorem pos_of_gt {M : Type u_1} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) :

0 < m

source

@[instance]

def canonically_linear_ordered_add_monoid.to_linear_order (α : Type u_1) [self : canonically_linear_ordered_add_monoid α] :

linear_order α

source

@[instance]

def canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid (α : Type u_1) [self : canonically_linear_ordered_add_monoid α] :

canonically_ordered_add_monoid α

source

@[class]

structure canonically_linear_ordered_add_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), canonically_linear_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_add_monoid.nsmul n.succ x = x + canonically_linear_ordered_add_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1
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

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

Instances

source

@[instance]

def canonically_linear_ordered_monoid.to_linear_order (α : Type u_1) [self : canonically_linear_ordered_monoid α] :

linear_order α

source

@[instance]

def canonically_linear_ordered_monoid.to_canonically_ordered_monoid (α : Type u_1) [self : canonically_linear_ordered_monoid α] :

canonically_ordered_monoid α

source

@[class]

structure canonically_linear_ordered_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), canonically_linear_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_monoid.npow n.succ x = x * canonically_linear_ordered_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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * c_1
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

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

source

@[instance]

def canonically_linear_ordered_add_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_add_monoid α] :

semilattice_sup_bot α

source

@[instance]

def canonically_linear_ordered_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_monoid α] :

semilattice_sup_bot α

Equations

canonically_linear_ordered_monoid.semilattice_sup_bot = {bot := order_bot.bot (canonically_ordered_monoid.to_order_bot α), le := lattice.le lattice_of_linear_order, lt := lattice.lt lattice_of_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup lattice_of_linear_order, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def with_top.canonically_linear_ordered_add_monoid (α : Type u_1) [canonically_linear_ordered_add_monoid α] :

canonically_linear_ordered_add_monoid (with_top α)

Equations

with_top.canonically_linear_ordered_add_monoid α = {add := canonically_ordered_add_monoid.add infer_instance, add_assoc := _, zero := canonically_ordered_add_monoid.zero infer_instance, zero_add := _, add_zero := _, nsmul := canonically_ordered_add_monoid.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := canonically_ordered_add_monoid.le infer_instance, lt := canonically_ordered_add_monoid.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := canonically_ordered_add_monoid.bot infer_instance, bot_le := _, le_iff_exists_add := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance}

source

theorem min_add_distrib {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :

min a (b + c) = min a (min a b + min a c)

source

theorem min_mul_distrib {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :

min a (b * c) = min a ((min a b) * min a c)

source

theorem min_mul_distrib' {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :

min (a * b) c = min ((min a c) * min b c) c

source

theorem min_add_distrib' {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :

min (a + b) c = min (min a c + min b c) c

source

@[class]

structure ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1

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

Instances

source

@[instance]

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

add_cancel_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_cancel_comm_monoid (α : Type u) [self : ordered_cancel_comm_monoid α] :

cancel_comm_monoid α

source

@[class]

structure ordered_cancel_comm_monoid (α : Type u) :

Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1

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

Instances

source

@[instance]

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

ordered_add_comm_monoid α

source

@[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 := _, lt_of_mul_lt_mul_left := _}

source

def function.injective.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

ordered_cancel_add_comm_monoid β

Pullback an ordered_cancel_add_comm_monoid under an injective map.

source

def function.injective.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

ordered_cancel_comm_monoid β

Pullback an ordered_cancel_comm_monoid under an injective map. See note [reducible non-instances].

Equations

function.injective.ordered_cancel_comm_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (a + c < a + b ↔ c < b)

source

theorem with_bot.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (a + c < a + b ↔ c < b)

source

theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (c + a < b + a ↔ c < b)

source

theorem with_bot.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (c + a < b + a ↔ c < b)

source

theorem fn_min_mul_fn_max {α : Type u} {β : Type u_1} [linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :

(f (min n m)) * f (max n m) = (f n) * f m

source

theorem fn_min_add_fn_max {α : Type u} {β : Type u_1} [linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :

f (min n m) + f (max n m) = f n + f m

source

theorem min_add_max {α : Type u} [linear_order α] [add_comm_semigroup α] (n m : α) :

min n m + max n m = n + m

source

theorem min_mul_max {α : Type u} [linear_order α] [comm_semigroup α] (n m : α) :

(min n m) * max n m = n * m

source

@[class]

structure linear_ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
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
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

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

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_1 : α), (a * b) * c_1 = a * b * c_1
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1
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
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

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

Instances

source

theorem min_mul_mul_left {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

min (a * b) (a * c) = a * min b c

source

theorem min_add_add_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + b) (a + c) = a + min b c

source

theorem min_add_add_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + c) (b + c) = min a b + c

source

theorem min_mul_mul_right {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

min (a * c) (b * c) = (min a b) * c

source

theorem max_add_add_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + b) (a + c) = a + max b c

source

theorem max_mul_mul_left {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

max (a * b) (a * c) = a * max b c

source

theorem max_mul_mul_right {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

max (a * c) (b * c) = (max a b) * c

source

theorem max_add_add_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + c) (b + c) = max a b + c

source

theorem min_le_add_of_nonneg_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (hb : 0 ≤ b) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_right {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (hb : 1 ≤ b) :

min a b ≤ a * b

source

theorem min_le_add_of_nonneg_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_left {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) :

min a b ≤ a * b

source

theorem max_le_mul_of_one_le {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

max a b ≤ a * b

source

theorem max_le_add_of_nonneg {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

max a b ≤ a + b

source

def function.injective.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

linear_ordered_cancel_comm_monoid β

Pullback a linear_ordered_cancel_comm_monoid under an injective map. See note [reducible non-instances].

Equations