Pulling back ordered rings along injective maps #
theorem
Function.Injective.isOrderedRing
{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)
[IsOrderedRing 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)
:
Pullback an IsOrderedRing under an injective map.
theorem
Function.Injective.isStrictOrderedRing
{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)
:
Pullback a IsStrictOrderedRing under an injective map.
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.orderedSemiring
{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)
[IsOrderedRing 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.isOrderedRing.
Pullback an IsOrderedRing under an injective map.
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.orderedCommSemiring
{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)
[IsOrderedRing 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.isOrderedRing.
Pullback an IsOrderedRing under an injective map.
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.orderedRing
{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)
[IsOrderedRing 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.isOrderedRing.
Pullback an IsOrderedRing under an injective map.
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.orderedCommRing
{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)
[IsOrderedRing 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.isOrderedRing.
Pullback an IsOrderedRing under an injective map.
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem
Function.Injective.strictOrderedSemiring
{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.strictOrderedCommSemiring
{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.strictOrderedRing
{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.strictOrderedCommRing
{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.linearOrderedSemiring
{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.linearOrderedCommSemiring
{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.linearOrderedRing
{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.linearOrderedCommRing
{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.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.