of'_commute — Mathlib

English

For any AddZeroClass M, the embedding of an element a ∈ M via of' commutes with any additive element f ∈ AddMonoidAlgebra R M provided a commutes with every a' in M.

Русский

Для любого AddZeroClass M отображение через of' элемента a коммутирует с любым элементом f ∈ AddMonoidAlgebra R M, если a коммутирует с каждым элементом M.

LaTeX

$$$\\mathrm{of'}\\ R M a \\;\\mathrm{commutes}\\; f = f \\;\\mathrm{commutes}\\; \\mathrm{of'}\\ R M a$ (при условии, что $a$ commute с всеми $a' \\in M$).$$

Lean4

theorem of'_commute [AddZeroClass M] {a : M} (h : ∀ a', AddCommute a a') (f : AddMonoidAlgebra R M) :
    Commute (of' R M a) f :=
  single_commute h .one_left f

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