norm_sq_re_conj_add

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.norm_sq_re_conj_add

English

The same identity holds for conj x + x: ‖conj x + x‖^2 = Re(conj x + x)^2.

Русский

Та же формула для conj x + x: ‖conj x + x‖^2 = Re(conj x + x)^2.

LaTeX

$$$$ \\|\\overline{x} + x\\|^{2} = \\operatorname{Re}(\\overline{x} + x)^{2}. $$$$

Lean4

theorem norm_sq_re_conj_add (x : K) : ‖conj x + x‖ ^ 2 = re (conj x + x) ^ 2 := by rw [add_comm, norm_sq_re_add_conj]

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

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

Разделы

Аффилиация

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