function_semiconj_mul_left — Mathlib

English

If a,b,c are elements with a semiconjugating b to c (i.e., a b = c a), then the left-multiplication maps x ↦ a x and x ↦ b x are semiconjugate by x ↦ c x; equivalently, for all x, a (b x) = c (a x).

Русский

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

LaTeX

$$$ \\text{SemiconjBy } a b c \\Rightarrow \\text{Semiconj } (a \\cdot \\cdot) (b \\cdot \\cdot) (c \\cdot \\cdot) $$$

Lean4

@[to_additive]
theorem function_semiconj_mul_left (h : SemiconjBy a b c) : Semiconj (a * ·) (b * ·) (c * ·) := fun j ↦ by
  simp only [← mul_assoc, h.eq]

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