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.