instIsOrderedRing — Mathlib

English

NatOrdinal carries the structure of an ordered ring: addition and multiplication interact with the order as in a ring.

Русский

NatOrdinal имеет структуру упорядоченного кольца: сложение и умножение взаимодействуют с порядком как в кольце.

LaTeX

$$$IsOrderedRing(NatOrdinal)$$$

Lean4

instance : IsOrderedRing NatOrdinal :=
  { mul_le_mul_of_nonneg_left := fun _ _ c h _ => nmul_le_nmul_left h c
    mul_le_mul_of_nonneg_right := fun _ _ c h _ => nmul_le_nmul_right h c }

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