instIsOrderedRing — Mathlib

English

The opposite ring R^op inherits an ordered ring structure from R.

Русский

Обратное кольцо R^op наследует упорядоченное кольцо из R.

LaTeX

$$IsOrderedRing $(R^{\\mathrm{op}})$ given IsOrderedRing $R$$$

Lean4

instance [Semiring R] [PartialOrder R] [IsOrderedRing R] : IsOrderedRing Rᵐᵒᵖ
    where
  zero_le_one := zero_le_one (α := R)
  mul_le_mul_of_nonneg_left _ _ _ := mul_le_mul_of_nonneg_right (α := R)
  mul_le_mul_of_nonneg_right _ _ _ := mul_le_mul_of_nonneg_left (α := R)

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