nnnorm_star_mul_self

Mathlib.Analysis.CStarAlgebra.Basic

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

English

For any x, nnnorm(x⋆ x) = nnnorm(x) · nnnorm(x).

Русский

Для любого x: nnnorm(x⋆ x) = nnnorm(x) · nnnorm(x).

LaTeX

$$nnnorm_star_mul_self {x} : nnnorm (x^{\star} x) = (nnnorm x)^{2}$$

Lean4

theorem nnnorm_star_mul_self {x : E} : ‖x⋆ * x‖₊ = ‖x‖₊ * ‖x‖₊ :=
  Subtype.ext norm_star_mul_self

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

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

Разделы

Аффилиация

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