English
If a is a unit and SemiconjBy a⁻¹ x y, then SemiconjBy a⁻¹ (x) (y) implies SemiconjBy a and reverse symmetry with inversion on the left.
Русский
Если a является единицей и SemiconjBy a⁻¹ x y, тогда SemiconjBy a⁻¹ x y сохраняется при реверсивном слева инверсии.
LaTeX
$$$$\forall a\in M^{\times},\ x,y\in M:\ SemiconjBy a^{-1} x y \Rightarrow SemiconjBy x y a^{-1}.$$$
Lean4
/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`. -/
@[to_additive /-- If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to
`x`. -/
]
theorem units_inv_symm_left {a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x :=
calc
↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹) := by rw [Units.mul_inv_cancel_right]
_ = x * ↑a⁻¹ := by rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
