English
If for all a,b with a > 0 and b > 0 we have a b > 0, then the ring is a strictly ordered ring.
Русский
Если для всех a,b с a > 0 и b > 0 имеем ab > 0, то кольцо является строго упорядоченным кольцом.
LaTeX
$$$ (\\forall a,b,\\ 0 < a \\land 0 < b \\to 0 < a b) \\Rightarrow \\text{IsStrictOrderedRing } R. $$$
Lean4
theorem of_mul_pos [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R]
(mul_pos : ∀ a b : R, 0 < a → 0 < b → 0 < a * b) : IsStrictOrderedRing R
where
mul_lt_mul_of_pos_left a b c ab hc := by simpa only [mul_sub, sub_pos] using mul_pos _ _ hc (sub_pos.2 ab)
mul_lt_mul_of_pos_right a b c ab hc := by simpa only [sub_mul, sub_pos] using mul_pos _ _ (sub_pos.2 ab) hc
