isStrictOrderedRing — Mathlib

English

If there is an injective order-preserving map f : S → R from a semiring S with a compatible order into a IsStrictOrderedRing R, then S itself inherits a strict ordered ring structure.

Русский

Если существует инъективное отображение с сохраняющее порядок и операции из полугруппы S в кольцо R, которое является строго упорядоченным кольцом, то S тоже является строго упорядоченным кольцом.

LaTeX

$$$\exists f:S \to R\ \,\text{injective},\ f(0)=0,\ f(1)=1,\ f(x+y)=f(x)+f(y),\ f(xy)=f(x)f(y),\ x\le y \iff f(x) \le f(y),\ x

Lean4

/-- Pullback a `IsStrictOrderedRing` under an injective map. -/
protected theorem isStrictOrderedRing [IsStrictOrderedRing R] [Semiring S] [PartialOrder S] (f : S → R) (zero : f 0 = 0)
    (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y}, f x < f y ↔ x < y) : IsStrictOrderedRing S :=
  { __ := Function.Injective.isOrderedCancelAddMonoid f add le
    __ := domain_nontrivial f zero one
    __ := Function.Injective.isOrderedRing f zero one add mul le
    mul_lt_mul_of_pos_left a b c h
      hc := lt.1 <| by simpa only [mul, zero] using mul_lt_mul_of_pos_left (lt.2 h) (by rwa [← zero, lt])
    mul_lt_mul_of_pos_right a b c h
      hc := lt.1 <| by simpa only [mul, zero] using mul_lt_mul_of_pos_right (lt.2 h) (by rwa [← zero, lt]) }

Похожие утверждения