English
If a semiconjugates b y z and b semiconjugates x y, then (a b) semiconjugates x z; i.e., (a b) x = z (a b).
Русский
Если a полусопрягает y к z, а b — x к y, то a b полусопрягает x к z; то есть (a b) x = z (a b).
LaTeX
$$$$ha:\ SemiconjBy a y z\quad hb:\ SemiconjBy b x y\Rightarrow SemiconjBy (a b)\ x\ z.$$$$
Lean4
/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a * b`
semiconjugates `x` to `z`. -/
@[to_additive /-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a + b`
semiconjugates `x` to `z`. -/
]
theorem mul_left (ha : SemiconjBy a y z) (hb : SemiconjBy b x y) : SemiconjBy (a * b) x z :=
by
unfold SemiconjBy
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
