isStrictOrderedRing — Mathlib

English

ZNum carries a strict ordered ring structure; product of positive elements is positive.

Русский

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

LaTeX

$$$$ZNum\text{ is a strict ordered ring: } a>0\land b>0\Rightarrow ab>0.$$$$

Lean4

instance isStrictOrderedRing : IsStrictOrderedRing ZNum :=
  .of_mul_pos fun a b ↦ by
    transfer_rw
    apply mul_pos

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