Documentation

Mathlib.Algebra.Order.Group.InjSurj

Pull back ordered groups along injective maps. #

@[reducible, inline]
abbrev Function.Injective.orderedAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] {β : Type u_3} [Zero β] [Add β] [Neg β] [Sub β] [SMul β] [SMul β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (inv : ∀ (x : β), f (-x) = -f x) (div : ∀ (x y : β), f (x - y) = f x - f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (zpow : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback an OrderedAddCommGroup under an injective map.

Equations
Instances For
    @[reducible, inline]
    abbrev Function.Injective.orderedCommGroup {α : Type u_1} [OrderedCommGroup α] {β : Type u_3} [One β] [Mul β] [Inv β] [Div β] [Pow β ] [Pow β ] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : β), f (x / y) = f x / f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

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

    Equations
    Instances For
      @[reducible, inline]
      abbrev Function.Injective.linearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_3} [Zero β] [Add β] [Neg β] [Sub β] [SMul β] [SMul β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (inv : ∀ (x : β), f (-x) = -f x) (div : ∀ (x y : β), f (x - y) = f x - f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (zpow : ∀ (x : β) (n : ), f (n x) = n f x) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

      Pullback a LinearOrderedAddCommGroup under an injective map.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.Injective.linearOrderedCommGroup {α : Type u_1} [LinearOrderedCommGroup α] {β : Type u_3} [One β] [Mul β] [Inv β] [Div β] [Pow β ] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : β), f (x / y) = f x / f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

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

        Equations
        Instances For