algebra.order.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 : α), (a * b) * c = a * b * c
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 : α), 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

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b (multiplication is monotone)

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 : α), a + b + c = a + (b + c)
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 : α), 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

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b (addition is monotone)

Instances

source

@[protected, 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

@[protected, 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

@[protected, 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

@[protected, 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

theorem has_mul.to_covariant_class_left (M : Type u_1) [has_mul M] [partial_order M] [covariant_class M M has_mul.mul has_lt.lt] :

covariant_class M M has_mul.mul has_le.le

source

theorem has_add.to_covariant_class_left (M : Type u_1) [has_add M] [partial_order M] [covariant_class M M has_add.add has_lt.lt] :

covariant_class M M has_add.add has_le.le

source

theorem has_add.to_covariant_class_right (M : Type u_1) [has_add M] [partial_order M] [covariant_class M M (function.swap has_add.add) has_lt.lt] :

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

source

theorem has_mul.to_covariant_class_right (M : Type u_1) [has_mul M] [partial_order M] [covariant_class M M (function.swap has_mul.mul) has_lt.lt] :

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

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 : α), 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
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_add_comm_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_add_comm_monoid.min = min_default . "reflexivity"
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_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 : α), c + a ≤ c + b

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 : α), 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
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_comm_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_comm_monoid.min = min_default . "reflexivity"
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_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 : α), c * a ≤ c * b

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 : α), 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
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_comm_monoid_with_zero.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_comm_monoid_with_zero.min = min_default . "reflexivity"
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_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 : α), c * a ≤ c * b
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

@[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 : α), 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
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_add_comm_monoid_with_top.max = max_default . "reflexivity"
min : α → α → α
min_def : linear_ordered_add_comm_monoid_with_top.min = min_default . "reflexivity"
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_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 : α), c + a ≤ c + b
top : α
le_top : ∀ (x : α), x ≤ ⊤
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

@[instance]

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

has_top α

source

@[protected, instance]

def linear_ordered_add_comm_monoid_with_top.to_order_top (α : Type u) [h : linear_ordered_add_comm_monoid_with_top α] :

order_top α

Equations

linear_ordered_add_comm_monoid_with_top.to_order_top α = {top := linear_ordered_add_comm_monoid_with_top.top h, le_top := _}

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 β] [has_pow β ℕ] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :

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 npow = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul npow), 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 := _}

source

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

ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

Equations

function.injective.ordered_add_comm_monoid f hf one mul npow = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf one mul npow), add_assoc := _, zero := add_comm_monoid.zero (function.injective.add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_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 := _, add_le_add_left := _}

source

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

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 npow = {le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul npow), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul npow), 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), max := max (linear_order.lift f hf), max_def := _, min := min (linear_order.lift f hf), min_def := _, mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul npow), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_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 β] [has_scalar ℕ β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :

linear_ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

Equations

function.injective.linear_ordered_add_comm_monoid f hf one mul npow = {le := ordered_add_comm_monoid.le (function.injective.ordered_add_comm_monoid f hf one mul npow), lt := ordered_add_comm_monoid.lt (function.injective.ordered_add_comm_monoid f hf one mul npow), 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), max := max (linear_order.lift f hf), max_def := _, min := min (linear_order.lift f hf), min_def := _, add := ordered_add_comm_monoid.add (function.injective.ordered_add_comm_monoid f hf one mul npow), add_assoc := _, zero := ordered_add_comm_monoid.zero (function.injective.ordered_add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (function.injective.ordered_add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}

source

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

0 < bit0 a

source

@[protected, instance]

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

preorder (add_units α)

Equations

add_units.preorder = preorder.lift coe

source

@[protected, instance]

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

preorder αˣ

Equations

units.preorder = preorder.lift coe

source

@[simp, norm_cast]

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

↑a ≤ ↑b ↔ a ≤ b

source

@[simp, norm_cast]

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

↑a ≤ ↑b ↔ a ≤ b

source

@[simp, norm_cast]

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

↑a < ↑b ↔ a < b

source

@[simp, norm_cast]

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

↑a < ↑b ↔ a < b

source

@[protected, instance]

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

partial_order (add_units α)

Equations

add_units.partial_order = partial_order.lift coe add_units.ext

source

@[protected, instance]

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

partial_order αˣ

Equations

units.partial_order = partial_order.lift coe units.ext

source

@[protected, instance]

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

linear_order αˣ

Equations

units.linear_order = linear_order.lift coe units.ext

source

@[protected, instance]

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

linear_order (add_units α)

Equations

add_units.linear_order = linear_order.lift coe add_units.ext

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

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

source

@[protected, instance]

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

preorder (with_zero α)

Equations

with_zero.preorder = with_bot.preorder

source

@[protected, instance]

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

partial_order (with_zero α)

Equations

with_zero.partial_order = with_bot.partial_order

source

@[protected, instance]

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

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, norm_cast]

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

↑a < ↑b ↔ a < b

source

@[simp, norm_cast]

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

↑a ≤ ↑b ↔ a ≤ b

source

@[protected, instance]

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

lattice (with_zero α)

Equations

with_zero.lattice = with_bot.lattice

source

@[protected, 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

@[simp]

theorem with_zero.le_max_iff {α : Type u} [linear_order α] {a b c : α} :

↑a ≤ max ↑b ↑c ↔ a ≤ max b c

source

@[simp]

theorem with_zero.min_le_iff {α : Type u} [linear_order α] {a b c : α} :

min ↑a ↑b ≤ ↑c ↔ min a b ≤ c

source

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

source

@[protected]

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. See note [reducible non-instances].

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 := _}

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_has_bot (α : Type u_1) [self : canonically_ordered_add_monoid α] :

has_bot α

source

@[class]

structure canonically_ordered_add_monoid (α : Type u_1) :

Type u_1

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 : α), 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 : α), 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
bot : α
bot_le : ∀ (x : α), ⊥ ≤ x
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c : α), b = a + c

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

@[protected, instance]

def canonically_ordered_add_monoid.to_order_bot (α : Type u) [h : canonically_ordered_add_monoid α] :

order_bot α

Equations

canonically_ordered_add_monoid.to_order_bot α = {bot := canonically_ordered_add_monoid.bot h, bot_le := _}

source

@[instance]

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

ordered_comm_monoid α

source

@[instance]

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

has_bot α

source

@[class]

structure canonically_ordered_monoid (α : Type u_1) :

Type u_1

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 : α), 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 : α), 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
bot : α
bot_le : ∀ (x : α), ⊥ ≤ x
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c : α), b = a * c

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. Examples 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

source

@[protected, instance]

def canonically_ordered_monoid.to_order_bot (α : Type u) [h : canonically_ordered_monoid α] :

order_bot α

Equations

canonically_ordered_monoid.to_order_bot α = {bot := canonically_ordered_monoid.bot h, bot_le := _}

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 eq_zero_or_pos {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

a = 0 ∨ 0 < a

source

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

a = 1 ∨ 1 < a

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

theorem lt_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} [covariant_class α α has_mul.mul has_lt.lt] :

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

source

theorem lt_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} [covariant_class α α has_add.add has_lt.lt] :

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

source

@[protected, 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 := _, bot := order_bot.bot with_zero.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[protected, instance]

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

has_exists_mul_of_le α

source

@[protected, 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 : α), a + b + c = a + (b + c)
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 : α), 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
bot : α
bot_le : ∀ (x : α), ⊥ ≤ x
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c : α), b = a + 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 : canonically_linear_ordered_add_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : canonically_linear_ordered_add_monoid.min = min_default . "reflexivity"

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 : α), (a * b) * c = a * b * c
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 : α), 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
bot : α
bot_le : ∀ (x : α), ⊥ ≤ x
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c : α), b = a * 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 : canonically_linear_ordered_monoid.max = max_default . "reflexivity"
min : α → α → α
min_def : canonically_linear_ordered_monoid.min = min_default . "reflexivity"

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

source

@[protected, instance]

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

semilattice_sup α

Equations

canonically_linear_ordered_add_monoid.semilattice_sup = {sup := lattice.sup linear_order.to_lattice, le := lattice.le linear_order.to_lattice, lt := lattice.lt linear_order.to_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

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

semilattice_sup α

Equations

canonically_linear_ordered_monoid.semilattice_sup = {sup := lattice.sup linear_order.to_lattice, le := lattice.le linear_order.to_lattice, lt := lattice.lt linear_order.to_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

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

canonically_linear_ordered_add_monoid (with_zero α)

Equations

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

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

@[simp]

theorem one_min {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :

min 1 a = 1

source

@[simp]

theorem zero_min {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :

min 0 a = 0

source

@[simp]

theorem min_zero {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :

min a 0 = 0

source

@[simp]

theorem min_one {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :

min a 1 = 1

source

@[class]

structure ordered_cancel_add_comm_monoid (α : Type u) :

Type u

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

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 : α), (a * b) * c = a * b * c
mul_left_cancel : ∀ (a b c : α), a * b = a * c → 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

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

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

ordered_cancel_add_comm_monoid β

Pullback an ordered_cancel_add_comm_monoid under an injective map.

Equations

function.injective.ordered_cancel_add_comm_monoid f hf one mul npow = {add := add_left_cancel_semigroup.add (function.injective.add_left_cancel_semigroup f hf mul), add_assoc := _, add_left_cancel := _, zero := ordered_add_comm_monoid.zero (function.injective.ordered_add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (function.injective.ordered_add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le (function.injective.ordered_add_comm_monoid f hf one mul npow), lt := ordered_add_comm_monoid.lt (function.injective.ordered_add_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

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

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 npow = {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 npow), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul npow), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

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 : α), a + b + c = a + (b + c)
add_left_cancel : ∀ (a b c : α), a + b = a + c → 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

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
mul_left_cancel : ∀ (a b c : α), a * b = a * c → 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

source

theorem min_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :

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

source

theorem min_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :

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

source

theorem max_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :

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

source

theorem max_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :

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

source

theorem lt_or_lt_of_add_lt_add {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b m n : α} (h : m + n < a + b) :

m < a ∨ n < b

source

theorem lt_or_lt_of_mul_lt_mul {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b m n : α} (h : m * n < a * b) :

m < a ∨ n < b

source

theorem mul_lt_mul_iff_of_le_of_le {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (ac : a ≤ c) (bd : b ≤ d) :

a * b < c * d ↔ a < c ∨ b < d

source

theorem add_lt_add_iff_of_le_of_le {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (ac : a ≤ c) (bd : b ≤ d) :

a + b < c + d ↔ a < c ∨ b < d

source

theorem min_add_add_right {α : Type u} [linear_order α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b c : α) :

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

source

theorem min_mul_mul_right {α : Type u} [linear_order α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b c : α) :

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

source

theorem max_mul_mul_right {α : Type u} [linear_order α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b c : α) :

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

source

theorem max_add_add_right {α : Type u} [linear_order α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b c : α) :

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

source

theorem min_le_add_of_nonneg_right {α : Type u} [linear_order α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (hb : 0 ≤ b) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_right {α : Type u} [linear_order α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (hb : 1 ≤ b) :

min a b ≤ a * b

source

theorem min_le_add_of_nonneg_left {α : Type u} [linear_order α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 ≤ a) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_left {α : Type u} [linear_order α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 ≤ a) :

min a b ≤ a * b

source

theorem max_le_mul_of_one_le {α : Type u} [linear_order α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

max a b ≤ a * b

source

theorem max_le_add_of_nonneg {α : Type u} [linear_order α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {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 β] [has_pow β ℕ] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :

linear_ordered_cancel_comm_monoid β

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

Equations

function.injective.linear_ordered_cancel_comm_monoid f hf one mul npow = {mul := linear_ordered_comm_monoid.mul (function.injective.linear_ordered_comm_monoid f hf one mul npow), mul_assoc := _, mul_left_cancel := _, one := linear_ordered_comm_monoid.one (function.injective.linear_ordered_comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := linear_ordered_comm_monoid.npow (function.injective.linear_ordered_comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_ordered_comm_monoid.le (function.injective.linear_ordered_comm_monoid f hf one mul npow), lt := linear_ordered_comm_monoid.lt (function.injective.linear_ordered_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _, le_total := _, decidable_le := linear_ordered_comm_monoid.decidable_le (function.injective.linear_ordered_comm_monoid f hf one mul npow), decidable_eq := linear_ordered_comm_monoid.decidable_eq (function.injective.linear_ordered_comm_monoid f hf one mul npow), decidable_lt := linear_ordered_comm_monoid.decidable_lt (function.injective.linear_ordered_comm_monoid f hf one mul npow), max := linear_ordered_comm_monoid.max (function.injective.linear_ordered_comm_monoid f hf one mul npow), max_def := _, min := linear_ordered_comm_monoid.min (function.injective.linear_ordered_comm_monoid f hf one mul npow), min_def := _}

source

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

linear_ordered_cancel_add_comm_monoid β

Pullback a linear_ordered_cancel_add_comm_monoid under an injective map.

Equations

function.injective.linear_ordered_cancel_add_comm_monoid f hf one mul npow = {add := linear_ordered_add_comm_monoid.add (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), add_assoc := _, add_left_cancel := _, zero := linear_ordered_add_comm_monoid.zero (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := linear_ordered_add_comm_monoid.nsmul (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := linear_ordered_add_comm_monoid.le (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), lt := linear_ordered_add_comm_monoid.lt (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, le_total := _, decidable_le := linear_ordered_add_comm_monoid.decidable_le (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), decidable_eq := linear_ordered_add_comm_monoid.decidable_eq (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), decidable_lt := linear_ordered_add_comm_monoid.decidable_lt (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), max := linear_ordered_add_comm_monoid.max (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), max_def := _, min := linear_ordered_add_comm_monoid.min (function.injective.linear_ordered_add_comm_monoid f hf one mul npow), min_def := _}

source

@[protected, instance]

def order_dual.has_add {α : Type u} [h : has_add α] :

has_add (order_dual α)

Equations

order_dual.has_add = h

source

@[protected, instance]

def order_dual.has_mul {α : Type u} [h : has_mul α] :

has_mul (order_dual α)

Equations

order_dual.has_mul = h

source

@[protected, instance]

def order_dual.has_one {α : Type u} [h : has_one α] :

has_one (order_dual α)

Equations

order_dual.has_one = h

source

@[protected, instance]

def order_dual.add_semigroup {α : Type u} [h : add_semigroup α] :

add_semigroup (order_dual α)

Equations

order_dual.add_semigroup = h

source

@[protected, instance]

def order_dual.semigroup {α : Type u} [h : semigroup α] :

semigroup (order_dual α)

Equations

order_dual.semigroup = h

source

@[protected, instance]

def order_dual.add_comm_semigroup {α : Type u} [h : add_comm_semigroup α] :

add_comm_semigroup (order_dual α)

Equations

order_dual.add_comm_semigroup = h

source

@[protected, instance]

def order_dual.comm_semigroup {α : Type u} [h : comm_semigroup α] :

comm_semigroup (order_dual α)

Equations

order_dual.comm_semigroup = h

source

@[protected, instance]

def order_dual.mul_one_class {α : Type u} [h : mul_one_class α] :

mul_one_class (order_dual α)

Equations

order_dual.mul_one_class = h

source

@[protected, instance]

def order_dual.add_zero_class {α : Type u} [h : add_zero_class α] :

add_zero_class (order_dual α)

Equations

order_dual.add_zero_class = h

source

@[protected, instance]

def order_dual.add_monoid {α : Type u} [h : add_monoid α] :

add_monoid (order_dual α)

Equations

order_dual.add_monoid = h

source

@[protected, instance]

def order_dual.monoid {α : Type u} [h : monoid α] :

monoid (order_dual α)

Equations

order_dual.monoid = h

source

@[protected, instance]

def order_dual.comm_monoid {α : Type u} [h : comm_monoid α] :

comm_monoid (order_dual α)

Equations

order_dual.comm_monoid = h

source

@[protected, instance]

def order_dual.add_comm_monoid {α : Type u} [h : add_comm_monoid α] :

add_comm_monoid (order_dual α)

Equations

order_dual.add_comm_monoid = h

source

@[protected, instance]

def order_dual.left_cancel_monoid {α : Type u} [h : left_cancel_monoid α] :

left_cancel_monoid (order_dual α)

Equations

order_dual.left_cancel_monoid = h

source

@[protected, instance]

def order_dual.left_cancel_add_monoid {α : Type u} [h : add_left_cancel_monoid α] :

add_left_cancel_monoid (order_dual α)

Equations

order_dual.left_cancel_add_monoid = h

source

@[protected, instance]

def order_dual.right_cancel_monoid {α : Type u} [h : right_cancel_monoid α] :

right_cancel_monoid (order_dual α)

Equations

order_dual.right_cancel_monoid = h

source

@[protected, instance]

def order_dual.right_cancel_add_monoid {α : Type u} [h : add_right_cancel_monoid α] :

add_right_cancel_monoid (order_dual α)

Equations

order_dual.right_cancel_add_monoid = h

source

@[protected, instance]

def order_dual.cancel_monoid {α : Type u} [h : cancel_monoid α] :

cancel_monoid (order_dual α)

Equations

order_dual.cancel_monoid = h

source

@[protected, instance]

def order_dual.cancel_add_monoid {α : Type u} [h : add_cancel_monoid α] :

add_cancel_monoid (order_dual α)

Equations

order_dual.cancel_add_monoid = h

source

@[protected, instance]

def order_dual.cancel_add_comm_monoid {α : Type u} [h : add_cancel_comm_monoid α] :

add_cancel_comm_monoid (order_dual α)

Equations

order_dual.cancel_add_comm_monoid = h

source

@[protected, instance]

def order_dual.cancel_comm_monoid {α : Type u} [h : cancel_comm_monoid α] :

cancel_comm_monoid (order_dual α)

Equations

order_dual.cancel_comm_monoid = h

source

@[protected, instance]

def order_dual.mul_zero_class {α : Type u} [h : mul_zero_class α] :

mul_zero_class (order_dual α)

Equations

order_dual.mul_zero_class = h

source

@[protected, instance]

def order_dual.mul_zero_one_class {α : Type u} [h : mul_zero_one_class α] :

mul_zero_one_class (order_dual α)

Equations

order_dual.mul_zero_one_class = h

source

@[protected, instance]

def order_dual.monoid_with_zero {α : Type u} [h : monoid_with_zero α] :

monoid_with_zero (order_dual α)

Equations

order_dual.monoid_with_zero = h

source

@[protected, instance]

def order_dual.comm_monoid_with_zero {α : Type u} [h : comm_monoid_with_zero α] :

comm_monoid_with_zero (order_dual α)

Equations

order_dual.comm_monoid_with_zero = h

source

@[protected, instance]

def order_dual.cancel_comm_monoid_with_zero {α : Type u} [h : cancel_comm_monoid_with_zero α] :

cancel_comm_monoid_with_zero (order_dual α)

Equations

order_dual.cancel_comm_monoid_with_zero = h

source

@[protected, instance]

def order_dual.contravariant_class_mul_le {α : Type u} [has_le α] [has_mul α] [c : contravariant_class α α has_mul.mul has_le.le] :

contravariant_class (order_dual α) (order_dual α) has_mul.mul has_le.le

source

@[protected, instance]

def order_dual.contravariant_class_add_le {α : Type u} [has_le α] [has_add α] [c : contravariant_class α α has_add.add has_le.le] :

contravariant_class (order_dual α) (order_dual α) has_add.add has_le.le

source

@[protected, instance]

def order_dual.covariant_class_mul_le {α : Type u} [has_le α] [has_mul α] [c : covariant_class α α has_mul.mul has_le.le] :

covariant_class (order_dual α) (order_dual α) has_mul.mul has_le.le

source

@[protected, instance]

def order_dual.covariant_class_add_le {α : Type u} [has_le α] [has_add α] [c : covariant_class α α has_add.add has_le.le] :

covariant_class (order_dual α) (order_dual α) has_add.add has_le.le

source

@[protected, instance]

def order_dual.contravariant_class_swap_add_le {α : Type u} [has_le α] [has_add α] [c : contravariant_class α α (function.swap has_add.add) has_le.le] :

contravariant_class (order_dual α) (order_dual α) (function.swap has_add.add) has_le.le

source

@[protected, instance]

def order_dual.contravariant_class_swap_mul_le {α : Type u} [has_le α] [has_mul α] [c : contravariant_class α α (function.swap has_mul.mul) has_le.le] :

contravariant_class (order_dual α) (order_dual α) (function.swap has_mul.mul) has_le.le

source

@[protected, instance]

def order_dual.covariant_class_swap_add_le {α : Type u} [has_le α] [has_add α] [c : covariant_class α α (function.swap has_add.add) has_le.le] :

covariant_class (order_dual α) (order_dual α) (function.swap has_add.add) has_le.le

source

@[protected, instance]

def order_dual.covariant_class_swap_mul_le {α : Type u} [has_le α] [has_mul α] [c : covariant_class α α (function.swap has_mul.mul) has_le.le] :

covariant_class (order_dual α) (order_dual α) (function.swap has_mul.mul) has_le.le

source

@[protected, instance]

def order_dual.contravariant_class_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : contravariant_class α α has_mul.mul has_lt.lt] :

contravariant_class (order_dual α) (order_dual α) has_mul.mul has_lt.lt

source

@[protected, instance]

def order_dual.contravariant_class_add_lt {α : Type u} [has_lt α] [has_add α] [c : contravariant_class α α has_add.add has_lt.lt] :

contravariant_class (order_dual α) (order_dual α) has_add.add has_lt.lt

source

@[protected, instance]

def order_dual.covariant_class_add_lt {α : Type u} [has_lt α] [has_add α] [c : covariant_class α α has_add.add has_lt.lt] :

covariant_class (order_dual α) (order_dual α) has_add.add has_lt.lt

source

@[protected, instance]

def order_dual.covariant_class_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : covariant_class α α has_mul.mul has_lt.lt] :

covariant_class (order_dual α) (order_dual α) has_mul.mul has_lt.lt

source

@[protected, instance]

def order_dual.contravariant_class_swap_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : contravariant_class α α (function.swap has_mul.mul) has_lt.lt] :

contravariant_class (order_dual α) (order_dual α) (function.swap has_mul.mul) has_lt.lt

source

@[protected, instance]

def order_dual.contravariant_class_swap_add_lt {α : Type u} [has_lt α] [has_add α] [c : contravariant_class α α (function.swap has_add.add) has_lt.lt] :

contravariant_class (order_dual α) (order_dual α) (function.swap has_add.add) has_lt.lt

source

@[protected, instance]

def order_dual.covariant_class_swap_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : covariant_class α α (function.swap has_mul.mul) has_lt.lt] :

covariant_class (order_dual α) (order_dual α) (function.swap has_mul.mul) has_lt.lt

source

@[protected, instance]

def order_dual.covariant_class_swap_add_lt {α : Type u} [has_lt α] [has_add α] [c : covariant_class α α (function.swap has_add.add) has_lt.lt] :

covariant_class (order_dual α) (order_dual α) (function.swap has_add.add) has_lt.lt

source

@[protected, instance]

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

ordered_add_comm_monoid (order_dual α)

Equations

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

source

@[protected, instance]

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

ordered_comm_monoid (order_dual α)

Equations

order_dual.ordered_comm_monoid = {mul := comm_monoid.mul order_dual.comm_monoid, mul_assoc := _, one := comm_monoid.one order_dual.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow order_dual.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

@[protected, instance]

def order_dual.ordered_cancel_comm_monoid.to_contravariant_class {α : Type u} [ordered_cancel_comm_monoid α] :

contravariant_class (order_dual α) (order_dual α) has_mul.mul has_le.le

source

@[protected, instance]

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

contravariant_class (order_dual α) (order_dual α) has_add.add has_le.le

source

@[protected, instance]

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

ordered_cancel_comm_monoid (order_dual α)

Equations

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

source

@[protected, instance]

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

ordered_cancel_add_comm_monoid (order_dual α)

Equations

source

@[protected, instance]

def order_dual.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] :

linear_ordered_cancel_comm_monoid (order_dual α)

Equations

order_dual.linear_ordered_cancel_comm_monoid = {mul := ordered_cancel_comm_monoid.mul order_dual.ordered_cancel_comm_monoid, mul_assoc := _, mul_left_cancel := _, one := ordered_cancel_comm_monoid.one order_dual.ordered_cancel_comm_monoid, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow order_dual.ordered_cancel_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := max (order_dual.linear_order α), max_def := _, min := min (order_dual.linear_order α), min_def := _}

source

@[protected, instance]

def order_dual.linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_cancel_add_comm_monoid α] :

linear_ordered_cancel_add_comm_monoid (order_dual α)

Equations

order_dual.linear_ordered_cancel_add_comm_monoid = {add := ordered_cancel_add_comm_monoid.add order_dual.ordered_cancel_add_comm_monoid, add_assoc := _, add_left_cancel := _, zero := ordered_cancel_add_comm_monoid.zero order_dual.ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul order_dual.ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := max (order_dual.linear_order α), max_def := _, min := min (order_dual.linear_order α), min_def := _}

source

@[protected, instance]

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

linear_ordered_add_comm_monoid (order_dual α)

Equations

order_dual.linear_ordered_add_comm_monoid = {le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := max (order_dual.linear_order α), max_def := _, min := min (order_dual.linear_order α), min_def := _, add := ordered_add_comm_monoid.add order_dual.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero order_dual.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul order_dual.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}

source

@[protected, instance]

def order_dual.linear_ordered_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] :

linear_ordered_comm_monoid (order_dual α)

Equations

order_dual.linear_ordered_comm_monoid = {le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := max (order_dual.linear_order α), max_def := _, min := min (order_dual.linear_order α), min_def := _, mul := ordered_comm_monoid.mul order_dual.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one order_dual.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow order_dual.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _}

source

@[protected, instance]

def prod.ordered_cancel_comm_monoid {M : Type u_1} {N : Type u_2} [ordered_cancel_comm_monoid M] [ordered_cancel_comm_monoid N] :

ordered_cancel_comm_monoid (M × N)

Equations

prod.ordered_cancel_comm_monoid = {mul := cancel_comm_monoid.mul prod.cancel_comm_monoid, mul_assoc := _, mul_left_cancel := _, one := cancel_comm_monoid.one prod.cancel_comm_monoid, one_mul := _, mul_one := _, npow := cancel_comm_monoid.npow prod.cancel_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (prod.partial_order M N), lt := partial_order.lt (prod.partial_order M N), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

@[protected, instance]

def prod.ordered_cancel_add_comm_monoid {M : Type u_1} {N : Type u_2} [ordered_cancel_add_comm_monoid M] [ordered_cancel_add_comm_monoid N] :

ordered_cancel_add_comm_monoid (M × N)

Equations

prod.ordered_cancel_add_comm_monoid = {add := add_cancel_comm_monoid.add prod.cancel_add_comm_monoid, add_assoc := _, add_left_cancel := _, zero := add_cancel_comm_monoid.zero prod.cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_cancel_comm_monoid.nsmul prod.cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le (prod.partial_order M N), lt := partial_order.lt (prod.partial_order M N), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

@[protected, instance]

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

has_one (with_top α)

Equations

with_top.has_one = {one := ↑1}

source

@[protected, instance]

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

has_zero (with_top α)

Equations

with_top.has_zero = {zero := ↑0}

source

@[simp, norm_cast]

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

↑1 = 1

source

@[simp, norm_cast]

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

↑0 = 0

source

@[simp, norm_cast]

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

↑a = 0 ↔ a = 0

source

@[simp, norm_cast]

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

↑a = 1 ↔ a = 1

source

@[protected, simp]

theorem with_top.map_zero {α : Type u} [has_zero α] {β : Type u_1} (f : α → β) :

option.map f 0 = ↑(f 0)

source

@[protected, simp]

theorem with_top.map_one {α : Type u} [has_one α] {β : Type u_1} (f : α → β) :

option.map f 1 = ↑(f 1)

source

@[simp, norm_cast]

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

0 = ↑a ↔ a = 0

source

@[simp, norm_cast]

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

@[protected, 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 (has_add.add a) o₂)}

source

@[norm_cast]

theorem with_top.coe_add {α : Type u} [has_add α] {x y : α} :

↑(x + y) = ↑x + ↑y

source

@[norm_cast]

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

↑(bit0 x) = bit0 ↑x

source

@[norm_cast]

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

↑(bit1 a) = bit1 ↑a

source

@[simp]

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

⊤ + a = ⊤

source

@[simp]

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

a + ⊤ = ⊤

source

@[simp]

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

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

source

theorem with_top.add_ne_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

@[simp]

theorem with_top.add_coe_eq_top_iff {α : Type u} [has_add α] {x : with_top α} {y : α} :

x + ↑y = ⊤ ↔ x = ⊤

source

@[simp]

theorem with_top.coe_add_eq_top_iff {α : Type u} [has_add α] {x : α} {y : with_top α} :

↑x + y = ⊤ ↔ y = ⊤

source

@[protected, instance]

def with_top.covariant_class_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] :

covariant_class (with_top α) (with_top α) has_add.add has_le.le

source

@[protected, instance]

def with_top.covariant_class_swap_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] :

covariant_class (with_top α) (with_top α) (function.swap has_add.add) has_le.le

source

@[protected, instance]

def with_top.contravariant_class_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α has_add.add has_lt.lt] :

contravariant_class (with_top α) (with_top α) has_add.add has_lt.lt

source

@[protected, instance]

def with_top.contravariant_class_swap_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] :

contravariant_class (with_top α) (with_top α) (function.swap has_add.add) has_lt.lt

source

@[protected]

theorem with_top.le_of_add_le_add_left {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊤) (h : a + b ≤ a + c) :

b ≤ c

source

@[protected]

theorem with_top.le_of_add_le_add_right {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) (h : b + a ≤ c + a) :

b ≤ c

source

@[protected]

theorem with_top.add_lt_add_left {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊤) (h : b < c) :

a + b < a + c

source

@[protected]

theorem with_top.add_lt_add_right {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊤) (h : b < c) :

b + a < c + a

source

@[protected]

theorem with_top.add_le_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊤) :

a + b ≤ a + c ↔ b ≤ c

source

@[protected]

theorem with_top.add_le_add_iff_right {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) :

b + a ≤ c + a ↔ b ≤ c

source

@[protected]

theorem with_top.add_lt_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊤) :

a + b < a + c ↔ b < c

source

@[protected]

theorem with_top.add_lt_add_iff_right {α : Type u} [has_add α] {a b c : with_top α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊤) :

b + a < c + a ↔ b < c

source

@[protected]

theorem with_top.add_lt_add_of_le_of_lt {α : Type u} [has_add α] {a b c d : with_top α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) (hab : a ≤ b) (hcd : c < d) :

a + c < b + d

source

@[protected]

theorem with_top.add_lt_add_of_lt_of_le {α : Type u} [has_add α] {a b c d : with_top α} [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hc : c ≠ ⊤) (hab : a < b) (hcd : c ≤ d) :

a + c < b + d

source

@[protected, 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

@[protected, 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_semigroup.add with_top.add_semigroup, add_assoc := _, add_comm := _}

source

@[protected, instance]

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

add_zero_class (with_top α)

Equations

with_top.add_zero_class = {zero := 0, add := has_add.add with_top.has_add, zero_add := _, add_zero := _}

source

@[protected, instance]

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

add_monoid (with_top α)

Equations

with_top.add_monoid = {add := add_zero_class.add with_top.add_zero_class, add_assoc := _, zero := add_zero_class.zero with_top.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (with_top α)), nsmul_zero' := _, nsmul_succ' := _}

source

@[protected, instance]

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

add_comm_monoid (with_top α)

Equations

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

source

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

source

@[protected, 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 := linear_order.le with_top.linear_order, lt := linear_order.lt with_top.linear_order, 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, max := max with_top.linear_order, max_def := _, min := min with_top.linear_order, min_def := _, 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 := _, top := order_top.top with_top.order_top, le_top := _, top_add' := _}

source

@[protected, 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 := ordered_add_comm_monoid.le with_top.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt with_top.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot with_top.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[protected, instance]

def with_top.canonically_linear_ordered_add_monoid {α : Type u} [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 with_top.canonically_ordered_add_monoid, add_assoc := _, zero := canonically_ordered_add_monoid.zero with_top.canonically_ordered_add_monoid, zero_add := _, add_zero := _, nsmul := canonically_ordered_add_monoid.nsmul with_top.canonically_ordered_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := canonically_ordered_add_monoid.le with_top.canonically_ordered_add_monoid, lt := canonically_ordered_add_monoid.lt with_top.canonically_ordered_add_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := canonically_ordered_add_monoid.bot with_top.canonically_ordered_add_monoid, bot_le := _, le_iff_exists_add := _, 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, max := max with_top.linear_order, max_def := _, min := min with_top.linear_order, min_def := _}

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, norm_cast]

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

0 < ↑a ↔ 0 < a

source

@[protected, instance]

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

has_one (with_bot α)

Equations

with_bot.has_one = with_top.has_one

source

@[protected, instance]

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

has_zero (with_bot α)

Equations

with_bot.has_zero = with_top.has_zero

source

@[protected, instance]

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

has_add (with_bot α)

Equations

with_bot.has_add = with_top.has_add

source

@[protected, instance]

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

add_semigroup (with_bot α)

Equations

with_bot.add_semigroup = with_top.add_semigroup

source

@[protected, 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

@[protected, instance]

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

add_zero_class (with_bot α)

Equations

with_bot.add_zero_class = with_top.add_zero_class

source

@[protected, instance]

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

add_monoid (with_bot α)

Equations

with_bot.add_monoid = with_top.add_monoid

source

@[protected, 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

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

source

@[protected, instance]

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

linear_ordered_add_comm_monoid (with_bot α)

Equations

with_bot.linear_ordered_add_comm_monoid = {le := linear_order.le with_bot.linear_order, lt := linear_order.lt with_bot.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le with_bot.linear_order, decidable_eq := linear_order.decidable_eq with_bot.linear_order, decidable_lt := linear_order.decidable_lt with_bot.linear_order, max := max with_bot.linear_order, max_def := _, min := min with_bot.linear_order, min_def := _, add := ordered_add_comm_monoid.add with_bot.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_bot.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul with_bot.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}

source

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

↑1 = 1

source

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

↑0 = 0

source

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

↑a = 0 ↔ a = 0

source

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

↑a = 1 ↔ a = 1

source

@[protected]

theorem with_bot.map_zero {α : Type u} {β : Type u_1} [has_zero α] (f : α → β) :

option.map f 0 = ↑(f 0)

source

@[protected]

theorem with_bot.map_one {α : Type u} {β : Type u_1} [has_one α] (f : α → β) :

option.map f 1 = ↑(f 1)

source

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

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

source

theorem with_bot.coe_bit0 {α : Type u} [has_add α] {x : α} :

↑(bit0 x) = bit0 ↑x

source

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

↑(bit1 a) = bit1 ↑a

source

@[simp]

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

⊥ + a = ⊥

source

@[simp]

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

a + ⊥ = ⊥

source

@[simp]

theorem with_bot.add_eq_bot {α : Type u} [has_add α] {a b : with_bot α} :

a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥

source

theorem with_bot.add_ne_bot {α : Type u} [has_add α] {a b : with_bot α} :

a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥

source

theorem with_bot.bot_lt_add {α : Type u} [has_add α] [partial_order α] {a b : with_bot α} :

⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b

source

theorem with_bot.add_eq_coe {α : Type u} [has_add α] {a b : with_bot α} {x : α} :

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

source

@[simp]

theorem with_bot.add_coe_eq_bot_iff {α : Type u} [has_add α] {a : with_bot α} {y : α} :

a + ↑y = ⊥ ↔ a = ⊥

source

@[simp]

theorem with_bot.coe_add_eq_bot_iff {α : Type u} [has_add α] {b : with_bot α} {x : α} :

↑x + b = ⊥ ↔ b = ⊥

source

@[protected, instance]

def with_bot.covariant_class_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] :

covariant_class (with_bot α) (with_bot α) has_add.add has_le.le

source

@[protected, instance]

def with_bot.covariant_class_swap_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] :

covariant_class (with_bot α) (with_bot α) (function.swap has_add.add) has_le.le

source

@[protected, instance]

def with_bot.contravariant_class_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α has_add.add has_lt.lt] :

contravariant_class (with_bot α) (with_bot α) has_add.add has_lt.lt

source

@[protected, instance]

def with_bot.contravariant_class_swap_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] :

contravariant_class (with_bot α) (with_bot α) (function.swap has_add.add) has_lt.lt

source

@[protected]

theorem with_bot.le_of_add_le_add_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊥) (h : a + b ≤ a + c) :

b ≤ c

source

@[protected]

theorem with_bot.le_of_add_le_add_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊥) (h : b + a ≤ c + a) :

b ≤ c

source

@[protected]

theorem with_bot.add_lt_add_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊥) (h : b < c) :

a + b < a + c

source

@[protected]

theorem with_bot.add_lt_add_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊥) (h : b < c) :

b + a < c + a

source

@[protected]

theorem with_bot.add_le_add_iff_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊥) :

a + b ≤ a + c ↔ b ≤ c

source

@[protected]

theorem with_bot.add_le_add_iff_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊥) :

b + a ≤ c + a ↔ b ≤ c

source

@[protected]

theorem with_bot.add_lt_add_iff_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊥) :

a + b < a + c ↔ b < c

source

@[protected]

theorem with_bot.add_lt_add_iff_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊥) :

b + a < c + a ↔ b < c

source

@[protected]

theorem with_bot.add_lt_add_of_le_of_lt {α : Type u} [has_add α] {a b c d : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (hb : b ≠ ⊥) (hab : a ≤ b) (hcd : c < d) :

a + c < b + d

source

@[protected]

theorem with_bot.add_lt_add_of_lt_of_le {α : Type u} [has_add α] {a b c d : with_bot α} [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) :

a + c < b + d

source

@[protected, instance]

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

preorder (multiplicative α)

Equations

multiplicative.preorder = id

source

@[protected, instance]

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

preorder (additive α)

Equations

additive.preorder = id

source

@[protected, instance]

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

partial_order (multiplicative α)

Equations

multiplicative.partial_order = id

source

@[protected, instance]

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

partial_order (additive α)

Equations

additive.partial_order = id

source

@[protected, instance]

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

linear_order (multiplicative α)

Equations

multiplicative.linear_order = id

source

@[protected, instance]

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

linear_order (additive α)

Equations

additive.linear_order = id

source

@[protected, instance]

def multiplicative.ordered_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :

ordered_comm_monoid (multiplicative α)

Equations

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

source

@[protected, instance]

def additive.ordered_add_comm_monoid {α : Type u} [ordered_comm_monoid α] :

ordered_add_comm_monoid (additive α)

Equations

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

source

@[protected, instance]

def multiplicative.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

ordered_cancel_comm_monoid (multiplicative α)

Equations

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

source

@[protected, instance]

def additive.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

ordered_cancel_add_comm_monoid (additive α)

Equations

additive.ordered_cancel_add_comm_monoid = {add := add_left_cancel_semigroup.add additive.add_left_cancel_semigroup, add_assoc := _, add_left_cancel := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

@[protected, instance]

def multiplicative.linear_ordered_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] :

linear_ordered_comm_monoid (multiplicative α)

Equations

multiplicative.linear_ordered_comm_monoid = {le := linear_order.le multiplicative.linear_order, lt := linear_order.lt multiplicative.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, max := max multiplicative.linear_order, max_def := _, min := min multiplicative.linear_order, min_def := _, mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _}

source

@[protected, instance]

def additive.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] :

linear_ordered_add_comm_monoid (additive α)

Equations

additive.linear_ordered_add_comm_monoid = {le := linear_order.le additive.linear_order, lt := linear_order.lt additive.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, max := max additive.linear_order, max_def := _, min := min additive.linear_order, min_def := _, add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}

source

@[simp]

theorem additive.of_mul_le {α : Type u} [preorder α] {a b : α} :

⇑additive.of_mul a ≤ ⇑additive.of_mul b ↔ a ≤ b

source

@[simp]

theorem additive.of_mul_lt {α : Type u} [preorder α] {a b : α} :

⇑additive.of_mul a < ⇑additive.of_mul b ↔ a < b

source

@[simp]

theorem additive.to_mul_le {α : Type u} [preorder α] {a b : additive α} :

⇑additive.to_mul a ≤ ⇑additive.to_mul b ↔ a ≤ b

source

@[simp]

theorem additive.to_mul_lt {α : Type u} [preorder α] {a b : additive α} :

⇑additive.to_mul a < ⇑additive.to_mul b ↔ a < b

source

@[simp]

theorem multiplicative.of_add_le {α : Type u} [preorder α] {a b : α} :

⇑multiplicative.of_add a ≤ ⇑multiplicative.of_add b ↔ a ≤ b

source

@[simp]

theorem multiplicative.of_add_lt {α : Type u} [preorder α] {a b : α} :

⇑multiplicative.of_add a < ⇑multiplicative.of_add b ↔ a < b

source

@[simp]

theorem multiplicative.to_add_le {α : Type u} [preorder α] {a b : multiplicative α} :

⇑multiplicative.to_add a ≤ ⇑multiplicative.to_add b ↔ a ≤ b

source

@[simp]

theorem multiplicative.to_add_lt {α : Type u} [preorder α] {a b : multiplicative α} :

⇑multiplicative.to_add a < ⇑multiplicative.to_add b ↔ a < b

source

def with_zero.to_mul_bot {α : Type u} [has_add α] :

with_zero (multiplicative α) ≃* multiplicative (with_bot α)

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

Equations

with_zero.to_mul_bot = mul_equiv.refl (with_zero (multiplicative α))

source

@[simp]

theorem with_zero.to_mul_bot_zero {α : Type u} [has_add α] :

⇑with_zero.to_mul_bot 0 = ⇑multiplicative.of_add ⊥

source

@[simp]

theorem with_zero.to_mul_bot_coe {α : Type u} [has_add α] (x : multiplicative α) :

⇑with_zero.to_mul_bot ↑x = ⇑multiplicative.of_add ↑(⇑multiplicative.to_add x)

source

@[simp]

theorem with_zero.to_mul_bot_symm_bot {α : Type u} [has_add α] :

⇑(with_zero.to_mul_bot.symm) (⇑multiplicative.of_add ⊥) = 0

source

@[simp]

theorem with_zero.to_mul_bot_coe_of_add {α : Type u} [has_add α] (x : α) :

⇑(with_zero.to_mul_bot.symm) (⇑multiplicative.of_add ↑x) = ↑(⇑multiplicative.of_add x)

source

theorem with_zero.to_mul_bot_strict_mono {α : Type u} [has_add α] [preorder α] :

strict_mono ⇑with_zero.to_mul_bot

source

@[simp]

theorem with_zero.to_mul_bot_le {α : Type u} [has_add α] [preorder α] (a b : with_zero (multiplicative α)) :

⇑with_zero.to_mul_bot a ≤ ⇑with_zero.to_mul_bot b ↔ a ≤ b

source

@[simp]

theorem with_zero.to_mul_bot_lt {α : Type u} [has_add α] [preorder α] (a b : with_zero (multiplicative α)) :

⇑with_zero.to_mul_bot a < ⇑with_zero.to_mul_bot b ↔ a < b

source

@[simp]

theorem order_embedding.add_left_apply {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α has_add.add has_lt.lt] (m n : α) :

⇑(order_embedding.add_left m) n = m + n

source

def order_embedding.mul_left {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (m : α) :

α ↪o α

The order embedding sending b to a * b, for some fixed a. See also order_iso.mul_left when working in an ordered group.

Equations

order_embedding.mul_left m = order_embedding.of_strict_mono (λ (n : α), m * n) _

source

def order_embedding.add_left {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α has_add.add has_lt.lt] (m : α) :

α ↪o α

The order embedding sending b to a + b, for some fixed a. See also order_iso.add_left when working in an additive ordered group.

Equations

order_embedding.add_left m = order_embedding.of_strict_mono (λ (n : α), m + n) _

source

@[simp]

theorem order_embedding.mul_left_apply {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (m n : α) :

⇑(order_embedding.mul_left m) n = m * n

source

@[simp]

theorem order_embedding.mul_right_apply {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (m n : α) :

⇑(order_embedding.mul_right m) n = n * m

source

def order_embedding.mul_right {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (m : α) :

α ↪o α

The order embedding sending b to b * a, for some fixed a. See also order_iso.mul_right when working in an ordered group.

Equations

order_embedding.mul_right m = order_embedding.of_strict_mono (λ (n : α), n * m) _

source

@[simp]

theorem order_embedding.add_right_apply {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (m n : α) :

⇑(order_embedding.add_right m) n = n + m

source

def order_embedding.add_right {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (m : α) :

α ↪o α

The order embedding sending b to b + a, for some fixed a. See also order_iso.add_right when working in an additive ordered group.

Equations

order_embedding.add_right m = order_embedding.of_strict_mono (λ (n : α), n + m) _

mathlib documentation

Ordered monoids #

Implementation details #

Order dual #

`with_bot`/`with_top` #

`additive`/`multiplicative` #

Ordered monoids #

Implementation details #

Order dual #

with_bot/with_top #

additive/multiplicative #

`with_bot`/`with_top` #

`additive`/`multiplicative` #