nnnorm_mul_self

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.nnnorm_mul_self

English

Again, for self-adjoint x, nnnorm(x x) = nnnorm(x)².

Русский

Снова: самосопряжённое x; nnnorm(x x) = nnnorm(x)².

LaTeX

$$IsSelfAdjoint.nnnorm_mul_self {x} (hx : IsSelfAdjoint x) : nnnorm (x * x) = (nnnorm x) ^ 2$$

Lean4

theorem _root_.IsSelfAdjoint.nnnorm_mul_self {x : E} (hx : IsSelfAdjoint x) : ‖x * x‖₊ = ‖x‖₊ ^ 2 :=
  Subtype.ext hx.norm_mul_self

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

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

Разделы

Аффилиация

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