instOne

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.instOne

English

The unit element of the ring is the image of 1: 1_{Zsqrtd} = ofInt(1).

Русский

Единица кольца равна образу 1: 1_{Zsqrtd} = ofInt(1).

LaTeX

$$$1_{\mathbb{Z}\sqrt{d}} = \mathrm{ofInt}(1).$$$

Lean4

/-- The one of the ring -/
instance : One (ℤ√d) :=
  ⟨ofInt 1⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru