single_one_comm — Mathlib

English

The element single 1 r, coming from the coefficient ring, commutes with every element f of MonoidAlgebra R M when M is MulOneClass and R is commutative semiring.

Русский

Элемент single 1 r, полученный из кольца коэффициентов, коммутирует с любым элементом f MonoidAlgebra R M, если M обладает свойством MulOneClass, а R — коммутативное полукольцо.

LaTeX

$$$\\forall r \\in R, \\forall f \\in \\mathrm{MonoidAlgebra}(R,M),\\ (\\mathrm{single}\\, 1\\, r) * f = f * (\\mathrm{single}\\, 1\\, r).$$$

Lean4

@[to_additive (dont_translate := R)]
theorem single_one_comm [MulOneClass M] (r : R) (f : MonoidAlgebra R M) : single (1 : M) r * f = f * single (1 : M) r :=
  single_commute .one_left (.all _) f

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