nontrivial — Mathlib

English

For every integer d, the ring Z[√d] is nontrivial (it contains at least two distinct elements).

Русский

Для любого целого d кольцо Z[√d] ненулево (содержит по меньшей мере два различных элемента).

LaTeX

$$$$ \forall d \in \mathbb{Z},\ \exists x,y\in \mathbb{Z}[\sqrt{d}]\text{ with } x \neq y. $$$$

Lean4

instance nontrivial : Nontrivial (ℤ√d) :=
  ⟨⟨0, 1, Zsqrtd.ext_iff.not.mpr (by simp)⟩⟩

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