of_commute — Mathlib

English

If h(m') holds for all m', then the element of R M m commutes with f in MonoidAlgebra: the commutativity follows from basis commutativity.

Русский

Если верно, что m коммутирует с любым m' в M, то образ m коммутирует с любым элементом f в MonoidAlgebra.

LaTeX

$$$\forall f: MonoidAlgebra(R,M), \ Commute(\operatorname{of}(R,M,m), f)$$$

Lean4

theorem of_commute (h : ∀ m', Commute m m') (f : MonoidAlgebra R M) : Commute (of R M m) f :=
  single_commute h .one_left f

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