Commit 2026-04-09 11:11 9a9afee3

feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras (#37569) Let A be a C⋆-algebra, and let a b x : A. The Fuglede–Putnam–Rosenblum theorem states that if a and b are normal and x intertwines a and b (i.e., SemiconjBy x a b). Then x also intertwines star a and star b. Fuglede's original result was for a = b (i.e., if x commutes with a, then x also commutes with star a), and Putnam extended it to intertwining elements. Rosenblum later gave the elementary proof formalized here using Liouville's theorem. A version of the Fuglede–Putnam theorem also holds for unbounded operators, but it necessitates a different proof technique and holds in different generality than the one given here.