English
If hb₁ : Commute a b and hb₂ : Commute (star a) b, then for any f, Commute (cfcₙ f a) b.
Русский
Если a коммутирует с b и star a коммутирует с b, тогда для любого f, Commute (cfcₙ f a) b.
LaTeX
$$$\forall a,b:\ Commute a b \land Commute (star a) b \Rightarrow \forall f:\ 𝕜 \to 𝕜,\ 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 hf₀ ha ↦ hb₁.cfcₙHom ha hb₂ ⟨⟨_, hf.restrict⟩, hf₀⟩
