toIsStrictOrderedRing — Mathlib

English

In a strictly ordered ring, multiplication by a strictly positive element preserves strict inequality from the left.

Русский

В строго упорядоченном кольце умножение на строго положительный элемент слева сохраняет строгое неравенство.

LaTeX

$$$ (a < b) \\Rightarrow (c a) < (c b) \\text{ for } c > 0. $$$

Lean4

/-- Turn an ordered domain into a strict ordered ring. -/
instance (priority := 50) toIsStrictOrderedRing (R : Type*) [Ring R] [PartialOrder R] [IsOrderedRing R]
    [NoZeroDivisors R] [Nontrivial R] : IsStrictOrderedRing R :=
  .of_mul_pos fun _ _ ap bp ↦ (mul_nonneg ap.le bp.le).lt_of_ne' (mul_ne_zero ap.ne' bp.ne')

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