Semiconjugate elements of a semigroup
Main definitions
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].
This file provides only basic operations (mul_left, mul_right, inv_right etc). Other
operations (pow_right, field inverse etc) are in the files that define corresponding notions.
x is semiconjugate to y by a, if a * x = y * a.
Equations
- semiconj_by a x y = (a * x = y * a)
x is additive 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⁻¹.