function_commute_mul_right — Mathlib

English

If a and b commute, then the right-multiplication maps f(x) = x a and g(x) = x b commute as functions, i.e., for all x, (x b) a = (x a) b.

Русский

Если a и b коммутируют, то отображения f(x)=x a и g(x)=x b commute как функции; то есть для всех x выполняется (x b) a = (x a) b.

LaTeX

$$$ \\forall x,\\; (x b) a = (x a) b $$$

Lean4

@[to_additive]
theorem function_commute_mul_right (h : Commute a b) : Function.Commute (· * a) (· * b) :=
  SemiconjBy.function_semiconj_mul_right_swap h

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