ofInt

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

In the ring ℤ√d, the integer n is represented as n + 0√d.

Русский

В кольце ℤ√d целое число n представлено как n + 0·√d.

LaTeX

$$$\mathrm{ofInt}(n) = n + 0\cdot \sqrt{d} \quad \text{in } \mathbb{Z}[\sqrt{d}].$$$

Lean4

/-- Convert an integer to a `ℤ√d` -/
def ofInt (n : ℤ) : ℤ√d :=
  ⟨n, 0⟩

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

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

Разделы

Аффилиация

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