norm_mem_unitary_mul

Mathlib.Analysis.CStarAlgebra.Basic

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

English

If U ∈ unitary E, then ∥U A∥ = ∥A∥ for all A ∈ E.

Русский

Если U ∈ unitary(E), то для всех A ∈ E выполняется ∥U A∥ = ∥A∥.

LaTeX

$$$ \|U A\| = \|A\| $$$

Lean4

theorem norm_mem_unitary_mul {U : E} (A : E) (hU : U ∈ unitary E) : ‖U * A‖ = ‖A‖ :=
  norm_coe_unitary_mul ⟨U, hU⟩ A

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

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

Разделы

Аффилиация

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