norm_def

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

The norm is defined by N(n) = n.re^2 − d n.im^2 for n ∈ ℤ√d.

Русский

Норма определяется как N(n) = n_{\re}^2 − d n_{\im}^2 для n ∈ ℤ√d.

LaTeX

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

Lean4

theorem norm_def (n : ℤ√d) : n.norm = n.re * n.re - d * n.im * n.im :=
  rfl

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

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

Разделы

Аффилиация

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