abs_norm

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

If d ≤ 0, then |norm(n)| = norm(n) for all n.

Русский

Если $d \\le 0$, то $|\\operatorname{norm}(n)| = \\operatorname{norm}(n)$ для всех $n$.

LaTeX

$$(d \\le 0) \\Rightarrow |\\operatorname{norm}(n)| = \\operatorname{norm}(n)$$

Lean4

@[simp]
theorem abs_norm (hd : d ≤ 0) (n : ℤ√d) : |n.norm| = n.norm :=
  abs_of_nonneg <| norm_nonneg hd n

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

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

Разделы

Аффилиация

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