English
Over the real numbers, if a and b commute and a* commutes with b, then for any real-valued function f, cfc f a commutes with b.
Русский
Переменная основана на реальных числах: если a и b коммутируют и a* коммутирует с b, то для любой real-функции f, cfc f a коммутирует с b.
LaTeX
$$$\forall a,b \in A\, (hb:\ Commute a b) (hb': Commute (a^*) b) (f: \mathbb{R} \to \mathbb{R}),\ Commute( cfc\! f\ a, b).$$
Lean4
/-- A version of `Commute.cfc` or `IsSelfAdjoint.commute_cfc` which does not require any interaction
with `star` when the base ring is `ℝ`. -/
@[grind ←]
protected theorem cfc_real {a b : A} (hb : Commute a b) (f : ℝ → ℝ) : Commute (cfc f a) b :=
cfc_cases (fun x ↦ Commute x b) a f (Commute.zero_left _) fun hf ha ↦
by
rw [← cfc_apply ..]
exact hb.cfc (ha.star_eq.symm ▸ hb) _
