instIsStrictOrderedRingCastInt — Mathlib

English

The ring ℤ√d is a strictly ordered ring, i.e., a well-behaved ordered ring with positivity properties (via multiplication).

Русский

Кольцо ℤ√d является строго упорядоченным кольцом, т.е. упорядоченное кольцо с позитивностью в умножении.

LaTeX

$$$$\text{IsStrictOrderedRing}(\mathbb{Z}\sqrt{d}).$$$$

Lean4

instance : IsStrictOrderedRing (ℤ√d) :=
  .of_mul_pos Zsqrtd.mul_pos

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