English
In any group G, SemiconjBy (b a b^{-1}) (b x b^{-1}) (b y b^{-1}) holds if and only if SemiconjBy a x y holds; i.e., conjugation by b preserves semiconjugacy relations.
Русский
В группе G сопоставление через сопряжение консервативно сохраняет отношение полусопряжённости: SemiconjBy (b a b^{-1}) (b x b^{-1}) (b y b^{-1}) эквивалентно SemiconjBy a x y.
LaTeX
$$$\\text{SemiconjBy}(b a b^{-1},\\, b x b^{-1},\\, b y b^{-1}) \\iff \\text{SemiconjBy}(a, x, y)$$$
Lean4
@[to_additive (attr := simp)]
theorem conj_iff {a x y b : G} : SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y :=
by
unfold SemiconjBy
simp only [← mul_assoc, inv_mul_cancel_right]
repeat rw [mul_assoc]
rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
