Theorems · Theorem · functional analysis

CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary

∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (x : A) (hx : x ≠ 0),
  have u₁ := selfAdjoint.unitarySelfAddISMul (realPart (‖x‖⁻¹ • x)) ⋯;
  have u₂ := selfAdjoint.unitarySelfAddISMul (imaginaryPart (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + Complex.I • (↑u₂ + ↑(star u₂)))

A stepping stone to CStarAlgebra.exists_sum_four_unitary that specifies the unitary elements precisely. The lets in the statement are intentional.

Defined in

Mathlib.Analysis.CStarAlgebra.Unitary.Span

Cited by

1 results in Mathlib

Foundations

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

Assumes

CStarAlgebraPartialOrderStarOrderedRing