English
If an element b commutes with a and with its adjoint a*, then b commutes with cfc f a for any function f.
Русский
Если элемент b коммутирует с a и с сопряженным к нему a*, то b коммутирует с cfc f a для любой функции f.
LaTeX
$$$\forall a,b \in A,\ Commute\! a \! b \land \ Commute\! (a^*) \! b \Rightarrow \forall f:\mathbb{K}\to\mathbb{K},\ Commute( cfc\! f\ a, b).$$
Lean4
/-- An element commutes with `cfc f a` if it commutes with both `a` and `star a`.
If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfc_real` or `Commute.cfc_nnreal` which don't require
the `Commute (star a) b` hypothesis. -/
@[grind ←]
protected theorem cfc {a b : A} (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : 𝕜 → 𝕜) : Commute (cfc f a) b :=
cfc_cases (fun x ↦ Commute x b) a f (Commute.zero_left _) fun hf ha ↦ hb₁.cfcHom ha hb₂ ⟨_, hf.restrict⟩
