We say that x is semiconjugate to y by a (semiconj_by a x y), if a * x = y * a. In this file we provide operations on semiconj_by _ _ _.
In the names of these operations, we treat a as the “left” argument, and both x and y as “right” arguments. This way most names in this file agree with the names of the corresponding lemmas for commute a b = semiconj_by a b b. As a side effect, some lemmas have only _right version.
Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(h.pow_right 5).eq] rather than just rw [h.pow_right 5].
x is semiconjugate to y by a, if a * x = y * a.
Equality behind semiconj_by a x y; useful for rewriting.
If a semiconjugates x to y and x' to y', then it semiconjugates x * x' to y * y'.
If both a and b semiconjugate x to y, then so does a * b.
Any element semiconjugates 1 to 1.
One semiconjugates any element to itself.
If a semiconjugates a unit x to a unit y, then it semiconjugates x⁻¹ to y⁻¹.
If a unit a semiconjugates x to y, then a⁻¹ semiconjugates y to x.
a semiconjugates x to a * x * a⁻¹.
a semiconjugates x to a * x * a⁻¹.