# Documentation

Mathlib.Algebra.Order.Monoid.Cancel.Basic

# Basic results on ordered cancellative monoids. #

We pull back ordered cancellative monoids along injective maps.

def Function.Injective.orderedCancelAddCommMonoid.proof_1 {α : Type u_1} [inst : ] {β : Type u_2} [inst : Add β] (f : βα) (mul : ∀ (x y : β), f (x + y) = f x + f y) (a : β) (b : β) (c : β) (bc : f (a + b) f (a + c)) :
f b f c
Equations
• (_ : f b f c) = (_ : f b f c)
def Function.Injective.orderedCancelAddCommMonoid {α : Type u} [inst : ] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : ] (f : βα) (hf : ) (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 OrderedCancelAddCommMonoid under an injective map.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.orderedCancelCommMonoid {α : Type u} [inst : ] {β : Type u_1} [inst : One β] [inst : Mul β] [inst : Pow β ] (f : βα) (hf : ) (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 OrderedCancelCommMonoid under an injective map. See note [reducible non-instances].

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.linearOrderedCancelAddCommMonoid.proof_1 {α : Type u_2} [inst : ] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) (a : β) (b : β) :
a b b a
Equations
def Function.Injective.linearOrderedCancelAddCommMonoid.proof_3 {α : Type u_2} [inst : ] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) (a : β) (b : β) :
max a b = if a b then b else a
Equations
• (_ : ∀ (a b : β), max a b = if a b then b else a) = (_ : ∀ (a b : β), max a b = if a b then b else a)
def Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} [inst : ] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedCancelAddCommMonoid under an injective map.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.linearOrderedCancelAddCommMonoid.proof_2 {α : Type u_2} [inst : ] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) (a : β) (b : β) :
min a b = if a b then a else b
Equations
• (_ : ∀ (a b : β), min a b = if a b then a else b) = (_ : ∀ (a b : β), min a b = if a b then a else b)
def Function.Injective.linearOrderedCancelCommMonoid {α : Type u} [inst : ] {β : Type u_1} [inst : One β] [inst : Mul β] [inst : Pow β ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

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

Equations
• One or more equations did not get rendered due to their size.