Theorems · Theorem · functional analysis
fuglede_putnam_rosenblum
∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] {a b x : A},
IsStarNormal a → IsStarNormal b → SemiconjBy x a b → SemiconjBy x (star a) (star b)Alias of SemiconjBy.star_right.
Fuglede–Putnam–Rosenblum: If a and b are normal elements in a C⋆-algebra A which
are interwined by x, then star a and star b are also intertwined by x.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Fuglede
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 293 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonUnitalCStarAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Star.starstatement · cited by 1,082
- NonUnitalCStarAlgebrastatement · cited by 149
- IsStarNormalstatement · cited by 117
- SemiconjBystatement · cited by 99
- SemiconjBy.star_rightproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.