Pulling back linearly ordered fields along injective maps #
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedSemifield
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[PartialOrder R]
[Zero S]
[One S]
[Add S]
[Mul S]
[SMul ℕ S]
[Pow S ℕ]
[NatCast S]
(f : S → R)
(hf : Injective f)
[IsStrictOrderedRing R]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : S), f (x + y) = f x + f y)
(mul : ∀ (x y : S), f (x * y) = f x * f y)
(nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x)
(npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
:
Alias of Function.Injective.isStrictOrderedRing.
Pullback a IsStrictOrderedRing under an injective map.
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedField
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[PartialOrder R]
[Zero S]
[One S]
[Add S]
[Mul S]
[SMul ℕ S]
[Pow S ℕ]
[NatCast S]
(f : S → R)
(hf : Injective f)
[IsStrictOrderedRing R]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : S), f (x + y) = f x + f y)
(mul : ∀ (x y : S), f (x * y) = f x * f y)
(nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x)
(npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
:
Alias of Function.Injective.isStrictOrderedRing.
Pullback a IsStrictOrderedRing under an injective map.