sqrtd

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

The representative of √d in the ring is ⟨0,1⟩.

Русский

Представление корня из d в кольце равно ⟨0,1⟩.

LaTeX

$$$\mathrm{sqrtd} = \langle 0, 1 \rangle \in \mathbb{Z}[\sqrt{d}].$$$

Lean4

/-- The representative of `√d` in the ring -/
def sqrtd : ℤ√d :=
  ⟨0, 1⟩

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

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

Разделы

Аффилиация

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