commute_cfcₙ — Mathlib

English

If a is self-adjoint and b commutes with a, then for every function f, the element cfcₙ f a commutes with b.

Русский

Если a самосопряжённый и b коммутирует с a, то для любой функции f элемент cfcₙ f a коммутирует с b.

LaTeX

$$$\\forall a,b\\in A\\;\\big(\\IsSelfAdjoint(a) \\land Commute(a,b) \\big) \\rightarrow \\forall f: \\mathbb{K} \\to \\mathbb{K},\\ Commute(\\,cfcₙ f a\\, , b)$$$

Lean4

/-- For `a` selfadjoint, an element commutes with `cfcₙ f a` if it commutes with `a`.

If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfcₙ_real` or `Commute.cfcₙ_nnreal` which don't
require the `IsSelfAdjoint` hypothesis on `a` (due to the junk value `cfcₙ f a = 0`). -/
protected theorem commute_cfcₙ {a b : A} (ha : IsSelfAdjoint a) (hb₁ : Commute a b) (f : 𝕜 → 𝕜) :
    Commute (cfcₙ f a) b :=
  hb₁.cfcₙ (ha.star_eq.symm ▸ hb₁) f

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