le_antisymm — Mathlib

English

There exists a linear order on ℤ√d making it a linearly ordered ring, extending the given preorder.

Русский

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

LaTeX

$$$$\exists \le \text{ on } \mathbb{Z}\sqrt{d} \text{ such that } (\mathbb{Z}\sqrt{d}, \le) \text{ is a linear order extending } \text{preorder}. $$$$

Lean4

theorem le_antisymm {a b : ℤ√d} (ab : a ≤ b) (ba : b ≤ a) : a = b :=
  eq_of_sub_eq_zero <| nonneg_antisymm ba (by rwa [neg_sub])

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