Theorems · Definition · functional analysis

selfAdjoint.unitarySelfAddISMul

{A : Type u_1} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] → [StarOrderedRing A] → (a : ↥(selfAdjoint A)) → ‖a‖ ≤ 1 → ↥(unitary A)

For a selfadjoint with ‖a‖ ≤ 1, this is the unitary a + I • √(1 - a ^ 2).

Defined in

Mathlib.Analysis.CStarAlgebra.Unitary.Span

Cited by

6 results in Mathlib

Foundations

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

Assumes

CStarAlgebraPartialOrderStarOrderedRing