Documentation

Mathlib.Algebra.Order.Field.InjSurj

Pulling back linearly ordered fields along injective maps. #

def Function.Injective.linearOrderedSemifield {α : Type u_1} {β : Type u_2} [inst : LinearOrderedSemifield α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Pow β ] [inst : SMul β] [inst : NatCast β] [inst : Inv β] [inst : Div β] [inst : Pow β ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (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) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = 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 LinearOrderedSemifield under an injective map.

Equations
  • One or more equations did not get rendered due to their size.
def Function.Injective.linearOrderedField {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : Pow β ] [inst : SMul β] [inst : SMul β] [inst : SMul β] [inst : NatCast β] [inst : IntCast β] [inst : RatCast β] [inst : Inv β] [inst : Div β] [inst : Pow β ] [inst : Sup β] [inst : Inf β] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (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) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) (qsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) (rat_cast : ∀ (n : ), f n = 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 LinearOrderedField under an injective map.

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