function_commute_mul_left — Mathlib

English

If a and b commute, then the left-multiplication maps f(x) = a x and g(x) = b x commute as functions: f ∘ g = g ∘ f; i.e., for all x, a(bx) = b(ax).

Русский

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

LaTeX

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

Lean4

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

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