Pulling back linearly ordered fields along injective maps

@[reducible, inline]

abbrev Function.Injective.linearOrderedSemifield {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [SMul ℚ≥0 β] [NatCast β] [NNRatCast β] [Inv β] [Div β] [Pow β ℤ] [Max β] [Min β] (f : β → α) (hf : Function.Injective f) [LinearOrderedSemifield α] (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 : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x : β), f (q • x) = q • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q) (hsup : ∀ (x y : β), f (x ⊔ y) = f x ⊔ f y) (hinf : ∀ (x y : β), f (x ⊓ y) = f x ⊓ f y) : LinearOrderedSemifield β

Pullback a LinearOrderedSemifield under an injective map.

Equations

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

@[reducible, inline]

abbrev Function.Injective.linearOrderedField {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [Pow β ℕ] [SMul ℕ β] [SMul ℤ β] [SMul ℚ≥0 β] [SMul ℚ β] [NatCast β] [IntCast β] [NNRatCast β] [RatCast β] [Inv β] [Div β] [Pow β ℤ] [Max β] [Min β] (f : β → α) (hf : Function.Injective f) [LinearOrderedField α] (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 : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : β), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x : β), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x : β), f (q • x) = q • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) (nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q) (ratCast : ∀ (q : ℚ), f ↑q = ↑q) (hsup : ∀ (x y : β), f (x ⊔ y) = f x ⊔ f y) (hinf : ∀ (x y : β), f (x ⊓ y) = f x ⊓ f y) : LinearOrderedField β

Pullback a LinearOrderedField under an injective map.

Equations

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