cfc_commute_cfc — Mathlib

English

The images cfc f a and cfc g a commute: cfc f a and cfc g a commute in the sense of operator multiplication.

Русский

Образы cfc f a и cfc g a коммутируют: их произведения образуют коммутирующую пару.

LaTeX

$$Commute (cfc f a) (cfc g a)$$

Lean4

theorem cfc_commute_cfc (f g : R → R) (a : A) : Commute (cfc f a) (cfc g a) :=
  by
  refine cfc_cases (fun x ↦ Commute x (cfc g a)) a f (by simp) fun hf ha ↦ ?_
  refine cfc_cases (fun x ↦ Commute _ x) a g (by simp) fun hg _ ↦ ?_
  exact Commute.all _ _ |>.map _

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