nnnorm_star

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#nnnorm_star

English

For any x in a C*-algebra, the norm of x* x equals the square of the norm of x: ||x* x|| = ||x||^2.

Русский

Для любого x в C*-алгебре выполняется ||x* x|| = ||x||^2.

LaTeX

$$$\|x^{*} x\| = \|x\|^{2}$$$

Lean4

@[simp]
theorem nnnorm_star (x : E) : ‖star x‖₊ = ‖x‖₊ :=
  Subtype.ext <| norm_star _

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

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

Разделы

Аффилиация

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