Pulling back ordered rings along injective maps #
theorem Function.Injective.isOrderedRing {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Semiring S] [PartialOrder S] (f : S → 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) (le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y) :
Pullback an IsOrderedRing under an injective map.
theorem Function.Injective.isStrictOrderedRing {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Semiring S] [PartialOrder S] (f : S → 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) (le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : S}, f x < f y ↔ x < y) :
Pullback a IsStrictOrderedRing under an injective map.