English
If a semiconjugates a unit x to y, then it semiconjugates x^{-1} to y^{-1}.
Русский
Если единицы x и y полусопрягают a, то a полусопрягает x^{-1} к y^{-1}.
LaTeX
$$$$\forall a\in M,\; x,y\in M^{\times}:\ SemiconjBy\ a\ x\ y \Rightarrow SemiconjBy\ a\ x^{-1}\ y^{-1}.$$$$
Lean4
/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`. -/
@[to_additive /-- If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it
semiconjugates `-x` to `-y`. -/
]
theorem units_inv_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹ :=
calc
a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹ := by rw [Units.inv_mul_cancel_left]
_ = ↑y⁻¹ * a := by rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
