Semiconjugate elements of a semigroup #
Main definitions #
In the names of these operations, we treat
a as the “left” argument, and both
“right” arguments. This way most names in this file agree with the names of the corresponding lemmas
commute a b = semiconj_by a b b. As a side effect, some lemmas have only
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 (
inv_right etc). Other
pow_right, field inverse etc) are in the files that define corresponding notions.