norm

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

The norm map N: ℤ[√d] → ℤ is given by N(x + y√d) = x^2 − d y^2.

Русский

Карта нормы N: ℤ[√d] → ℤ задаётся как N(x + y√d) = x^2 − d y^2.

LaTeX

$$$\mathrm{norm}(n) = n_{\re}^{2} - d \cdot n_{\im}^{2}$$$

Lean4

/-- The norm of an element of `ℤ[√d]`. -/
def norm (n : ℤ√d) : ℤ :=
  n.re * n.re - d * n.im * n.im

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

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

Разделы

Аффилиация

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