Theorems · Theorem · functional analysis

Unitary.mem_pathComponentOne_iff

∀ {A : Type u_1} [inst : CStarAlgebra A] {u : ↥(unitary A)},
  u ∈ pathComponent 1 ↔ ∃ l, (List.map selfAdjoint.expUnitary l).prod = u

The path component of the identity in the unitary group of a C⋆-algebra is the set of unitaries that can be expressed as a product of exponential unitaries.

Defined in

Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Cited by

0 results in Mathlib

Foundations

Depth 322 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CStarAlgebra