instIsOrderedRing — Mathlib

English

The additive opposite R^a^o inherits an ordered ring structure from R.

Русский

Аддитивное противоположное R^a^o наследует упорядоченное кольцо от R.

LaTeX

$$IsOrderedRing $(R^{\\mathrm{aop}})$ from 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_left (α := R)
  mul_le_mul_of_nonneg_right _ _ _ := mul_le_mul_of_nonneg_right (α := R)

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