Pull back ordered groups along injective maps. #
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedCommGroup
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[One β]
[Mul β]
[Pow β ℕ]
(f : β → α)
(hf : 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)
:
let x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedAddCommGroup
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : 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)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedCommGroup
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[One β]
[Mul β]
[Pow β ℕ]
(f : β → α)
(hf : 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)
:
let x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedAddCommGroup
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : 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)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.