instOrderedRingOfIsStrictOrderedRing

English

An ordered ring is obtained from a strictly ordered ring by providing the necessary inherited order properties.

Русский

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

LaTeX

$$$ \\forall R [Semiring R] [PartialOrder R] [IsStrictOrderedRing R], \\text{IsOrderedRing } R. $$$

Lean4

instance [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Lean.Grind.OrderedRing R
    where
  zero_lt_one := zero_lt_one
  mul_lt_mul_of_pos_left := IsStrictOrderedRing.mul_lt_mul_of_pos_left _ _ _
  mul_lt_mul_of_pos_right := IsStrictOrderedRing.mul_lt_mul_of_pos_right _ _ _

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