commute_cfc — Mathlib

English

If a is self-adjoint and commutes with b, then for every f, cfcHom ha f commutes with b.

Русский

Если a самосопряжено и коммутирует с b, то для любого f cfcHom ha f коммутирует с b.

LaTeX

$$$\forall a,b \in A,\ IsSelfAdjoint(a)\to \Commute(a,b)\Rightarrow \forall f:\mathrm{C}(\mathrm{spectrum}(\mathbb{K},a),\mathbb{K}),\ Commute( cfcHom(a,f), 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

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