norm_conj

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

The norm is invariant under conjugation: norm(conj(x)) = norm(x).

Русский

Норма сохраняется при сопряжении: нормa(за противоположное) = норма(оригинала).

LaTeX

$$$\\operatorname{norm}(\\operatorname{star}(x)) = \\operatorname{norm}(x)$$$

Lean4

@[simp]
theorem norm_conj (x : ℤ√d) : (star x).norm = x.norm :=
  (Int.cast_inj (α := ℤ√d)).1 <| by simp [norm_eq_mul_conj, mul_comm]

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

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

Разделы

Аффилиация

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