norm_unitary_smul

Mathlib.Analysis.CStarAlgebra.Basic

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

English

For a unitary U and A ∈ E, the norm is preserved under the action U • A: ∥U • A∥ = ∥A∥.

Русский

Для унитарного элемента U и A ∈ E норма сохраняется под действием U • A: ∥U • A∥ = ∥A∥.

LaTeX

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

Lean4

@[simp]
theorem norm_unitary_smul (U : unitary E) (A : E) : ‖U • A‖ = ‖A‖ :=
  norm_coe_unitary_mul U A

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

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

Разделы

Аффилиация

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