norm_of_mem_unitary

Mathlib.Analysis.CStarAlgebra.Basic

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

English

If U lies in the unitary group of E, then ∥U∥ = 1.

Русский

Если U принадлежит группе унитарных элементов E, то ∥U∥ = 1.

LaTeX

$$$ \|U\| = 1 $$$

Lean4

@[simp]
theorem norm_of_mem_unitary [Nontrivial E] {U : E} (hU : U ∈ unitary E) : ‖U‖ = 1 :=
  norm_coe_unitary ⟨U, hU⟩

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

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

Разделы

Аффилиация

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