English
If a semiconjugates x to y and x' to y', then a semiconjugates x x' to y y'.
Русский
Если a полусопрягает x к y и x' — к y', то a полусопрягает x x' к y y'.
LaTeX
$$$$\\text{If } h:\\ SemiconjBy\\ a\\ x\\ y,\\ h': SemiconjBy\\ a\\ x'\\ y'\\Rightarrow SemiconjBy\\ a\\ (x x')\\ (y y').$$$$
Lean4
/-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x * x'` to `y * y'`. -/
@[to_additive (attr := simp) /-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x + x'` to `y + y'`. -/
]
theorem mul_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x * x') (y * y') :=
by
unfold SemiconjBy
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
