norm_self_mul_star

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#CStarRing.norm_self_mul_star

English

The same relation as above but written with a prime variant: ||x⋆ x|| = ||x⋆|| · ||x||.

Русский

Та же связь, записанная в виде формулы: ||x⋆ x|| = ||x⋆|| · ||x||.

LaTeX

$$$\|x^{\star} x\| = \|x^{\star}\| \cdot \|x\|$$$

Lean4

theorem norm_self_mul_star {x : E} : ‖x * x⋆‖ = ‖x‖ * ‖x‖ :=
  by
  nth_rw 1 [← star_star x]
  simp only [norm_star_mul_self, norm_star]

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

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

Разделы

Аффилиация

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