Basic results on ordered cancellative monoids. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We pull back ordered cancellative monoids along injective maps.
@[reducible]
def
function.injective.ordered_cancel_add_comm_monoid
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
[has_smul ℕ β]
(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) :
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 := 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 := _, 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 := _}
@[reducible]
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) :
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 := 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 := _, 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 := _}
@[reducible]
def
function.injective.linear_ordered_cancel_comm_monoid
{α : Type u}
[linear_ordered_cancel_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
[has_pow β ℕ]
[has_sup β]
[has_inf β]
(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)
(hsup : ∀ (x y : β), f (x ⊔ y) = linear_order.max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = linear_order.min (f x) (f y)) :
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 hsup hinf = {mul := linear_ordered_comm_monoid.mul (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), mul_assoc := _, one := linear_ordered_comm_monoid.one (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), one_mul := _, mul_one := _, npow := linear_ordered_comm_monoid.npow (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_ordered_comm_monoid.le (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), lt := linear_ordered_comm_monoid.lt (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), 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 hsup hinf), decidable_eq := linear_ordered_comm_monoid.decidable_eq (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), decidable_lt := linear_ordered_comm_monoid.decidable_lt (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), max := linear_ordered_comm_monoid.max (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), max_def := _, min := linear_ordered_comm_monoid.min (function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf), min_def := _}
@[reducible]
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_smul ℕ β]
[has_sup β]
[has_inf β]
(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)
(hsup : ∀ (x y : β), f (x ⊔ y) = linear_order.max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = linear_order.min (f x) (f y)) :
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 hsup hinf = {add := linear_ordered_add_comm_monoid.add (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), add_assoc := _, zero := linear_ordered_add_comm_monoid.zero (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), zero_add := _, add_zero := _, nsmul := linear_ordered_add_comm_monoid.nsmul (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), 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 hsup hinf), lt := linear_ordered_add_comm_monoid.lt (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), 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 hsup hinf), decidable_eq := linear_ordered_add_comm_monoid.decidable_eq (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), decidable_lt := linear_ordered_add_comm_monoid.decidable_lt (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), max := linear_ordered_add_comm_monoid.max (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), max_def := _, min := linear_ordered_add_comm_monoid.min (function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf), min_def := _}