English
If a partially ordered ring satisfies 0 ≤ ab whenever 0 ≤ a and 0 ≤ b, then the structure is an ordered ring.
Русский
Если в частично упорядоченном кольце выполняется 0 ≤ ab при 0 ≤ a и 0 ≤ b, то получится упорядоченное кольцо.
LaTeX
$$$ (\\forall a,b,\\ 0 \\le a \\land 0 \\le b \\to 0 \\le a b) \\Rightarrow \\text{IsOrderedRing } R.$$$
Lean4
theorem of_mul_nonneg [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R]
(mul_nonneg : ∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) : IsOrderedRing R
where
mul_le_mul_of_nonneg_left a b c ab hc := by simpa only [mul_sub, sub_nonneg] using mul_nonneg _ _ hc (sub_nonneg.2 ab)
mul_le_mul_of_nonneg_right a b c ab
hc := by simpa only [sub_mul, sub_nonneg] using mul_nonneg _ _ (sub_nonneg.2 ab) hc
