isStrictOrderedRing — Mathlib

English

Num is a strictly ordered ring: the order is compatible with addition and multiplication, and there exist distinct elements with different signs.

Русский

Num является строгопорядковым кольцом: порядок совместим с аддитивной и мультипликативной структурами; существуют элементы с разными знаками.

LaTeX

$$IsStrictOrderedRing Num$$

Lean4

instance isStrictOrderedRing : IsStrictOrderedRing Num :=
  { zero_le_one := by decide
    mul_lt_mul_of_pos_left := by
      intro a b c
      transfer_rw
      apply mul_lt_mul_of_pos_left
    mul_lt_mul_of_pos_right := by
      intro a b c
      transfer_rw
      apply mul_lt_mul_of_pos_right
    exists_pair_ne := ⟨0, 1, by decide⟩ }

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