SemiconjBy.inv_right₀

theorem SemiconjBy.inv_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹

This theorem states that for any type `G₀` that forms a group with zero, and for any elements `a`, `x`, and `y` of that group, if `x` is semiconjugate to `y` by `a` (which means that multiplying `a` with `x` equals multiplying `y` with `a`), then the inverse of `x` is semiconjugate to the inverse of `y` by `a`. In mathematical terms, if $a \cdot x = y \cdot a$, then it implies that $a \cdot x^{-1} = y^{-1} \cdot a$.

More concisely: If `a`, `x`, and `y` are elements of a group with identity, and `a` semiconjugates `x` and `y` (i.e., `a * x = y * a`), then `a` semiconjugates their inverses (i.e., `a * x⁻¹ = y⁻¹ * a`).