Documentation

Mathlib.Algebra.Order.Ring.InjSurj

Pulling back ordered rings along injective maps #

source
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) :
IsOrderedRing S

Pullback an IsOrderedRing under an injective map.

source
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) :
IsStrictOrderedRing S

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem Function.Injective.orderedSemiring {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) :
IsOrderedRing S

Alias of Function.Injective.isOrderedRing.

Pullback an IsOrderedRing under an injective map.

source
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem Function.Injective.orderedCommSemiring {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) :
IsOrderedRing S

Alias of Function.Injective.isOrderedRing.

Pullback an IsOrderedRing under an injective map.

source
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem Function.Injective.orderedRing {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) :
IsOrderedRing S

Alias of Function.Injective.isOrderedRing.

Pullback an IsOrderedRing under an injective map.

source
@[deprecated Function.Injective.isOrderedRing (since := "2025-04-10")]
theorem Function.Injective.orderedCommRing {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) :
IsOrderedRing S

Alias of Function.Injective.isOrderedRing.

Pullback an IsOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.strictOrderedSemiring {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.strictOrderedCommSemiring {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.strictOrderedRing {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.strictOrderedCommRing {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedSemiring {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCommSemiring {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedRing {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCommRing {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedSemifield {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.

source
@[deprecated Function.Injective.isStrictOrderedRing (since := "2025-04-10")]
theorem Function.Injective.linearOrderedField {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) :
IsStrictOrderedRing S

Alias of Function.Injective.isStrictOrderedRing.

Pullback a IsStrictOrderedRing under an injective map.