toIsOrderedRing — Mathlib

English

A semiring with an IsStrictOrderedRing structure yields an IsOrderedRing structure by providing monotone multiplication properties.

Русский

Полупорядоченное кольцо с IsStrictOrderedRing образованием порождает IsOrderedRing через свойства монотонности умножения.

LaTeX

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

Lean4

instance (priority := 100) toIsOrderedRing : IsOrderedRing R
    where
  __ := ‹IsStrictOrderedRing R›
  mul_le_mul_of_nonneg_left _ _ _ := mul_le_mul_of_nonneg_left
  mul_le_mul_of_nonneg_right _ _ _ := mul_le_mul_of_nonneg_right

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