instIsStrictOrderedRing — Mathlib

English

The real numbers form a strict ordered ring: positivity is preserved under multiplication and other usual properties hold.

Русский

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

LaTeX

$$$\text{IsStrictOrderedRing}(\mathbb{R})$$$

Lean4

instance instIsStrictOrderedRing : IsStrictOrderedRing ℝ :=
  .of_mul_pos fun a b ↦ by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos

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