Theorems · Theorem · functional analysis
SemiconjBy.star_right
∀ {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)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
- 2 results in Mathlib
- Foundations
- Depth 292 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexproof · cited by 5,565
- Star.starstatement and proof · cited by 1,082
- NonUnitalCStarAlgebrastatement and proof · cited by 149
- IsStarNormalstatement and proof · cited by 117
- Unitization.inrproof · cited by 109
- SemiconjBystatement and proof · cited by 99
- SemiconjBy.eqproof · cited by 18
- Unitization.inr_injectiveproof · cited by 9
- Unitization.inr_mulproof · cited by 9
- Unitization.inr_starproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- IsStarNormal.commute_star_rightproof · cited by 2
- fuglede_putnam_rosenblumproof · cited by 0