English
Let a, b, c be elements of a group. Then conjugation by b distributes over multiplication: b a b^{-1} · (b c b^{-1}) = b (a c) b^{-1}. In particular, conjugation by b is a group homomorphism.
Русский
Пусть a, b, c — элементы группы. Тогда сопряжение по b распространяется на произведение: b a b^{-1} · (b c b^{-1}) = b (a c) b^{-1}. В частности, сопряжение по b — гомоморфизм группы.
LaTeX
$$$\forall a,b,c \in \alpha,\ (b a b^{-1})(b c b^{-1}) = b(a c)b^{-1}$$$
Lean4
@[simp]
theorem conj_mul {a b c : α} : b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹ :=
(map_mul (MulAut.conj b) a c).symm
