instIsStrictOrderedRing — Mathlib

English

The natural numbers form a strictly ordered ring; all the standard order axioms hold.

Русский

Числа Натурала образуют строго ранжированное кольцо; все стандартные аксиомы порядка выполняются.

LaTeX

$$IsStrictOrderedRing $\\mathbb{N}$$$

Lean4

instance instIsStrictOrderedRing : IsStrictOrderedRing ℕ
    where
  add_le_add_left := @Nat.add_le_add_left
  le_of_add_le_add_left := @Nat.le_of_add_le_add_left
  zero_le_one := Nat.le_of_lt (Nat.zero_lt_succ 0)
  mul_lt_mul_of_pos_left := @Nat.mul_lt_mul_of_pos_left
  mul_lt_mul_of_pos_right := @Nat.mul_lt_mul_of_pos_right
  exists_pair_ne := ⟨0, 1, ne_of_lt Nat.zero_lt_one⟩

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