cfcₙ_real — Mathlib

English

If a and b commute, then for every f: Real→Real, cfcₙ f a commutes with b.

Русский

Если a и b коммутируют, то для любого f: ℝ→ℝ, cfcₙ f a коммутирует с b.

LaTeX

$$$\\forall a,b\\in A\\; Commute(a,b) \\rightarrow \\forall 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 hf0 ha ↦
    by
    rw [← cfcₙ_apply ..]
    exact hb.cfcₙ (ha.star_eq.symm ▸ hb) _

Похожие утверждения