# Semiconjugate elements of a semigroup #

## Main definitions #

We say that x is semiconjugate to y by a (SemiconjBy a x y), if a * x = y * a. In this file we provide operations on SemiconjBy _ _ _.

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 = SemiconjBy 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.

theorem AddSemiconjBy.addUnits_neg_right {M : Type u_1} [] {a : M} {x : } {y : } (h : AddSemiconjBy a x y) :

If a semiconjugates an additive unit x to an additive unit y, then it semiconjugates -x to -y.

theorem SemiconjBy.units_inv_right {M : Type u_1} [] {a : M} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) :

If a semiconjugates a unit x to a unit y, then it semiconjugates x⁻¹ to y⁻¹.

@[simp]
theorem AddSemiconjBy.addUnits_neg_right_iff {M : Type u_1} [] {a : M} {x : } {y : } :
@[simp]
theorem SemiconjBy.units_inv_right_iff {M : Type u_1} [] {a : M} {x : Mˣ} {y : Mˣ} :
SemiconjBy a x⁻¹ y⁻¹ SemiconjBy a x y
theorem AddSemiconjBy.addUnits_neg_symm_left {M : Type u_1} [] {a : } {x : M} {y : M} (h : AddSemiconjBy (a) x y) :

If an additive unit a semiconjugates x to y, then -a semiconjugates y to x.

theorem SemiconjBy.units_inv_symm_left {M : Type u_1} [] {a : Mˣ} {x : M} {y : M} (h : SemiconjBy (a) x y) :
SemiconjBy (a⁻¹) y x

If a unit a semiconjugates x to y, then a⁻¹ semiconjugates y to x.

@[simp]
theorem AddSemiconjBy.addUnits_neg_symm_left_iff {M : Type u_1} [] {a : } {x : M} {y : M} :
@[simp]
theorem SemiconjBy.units_inv_symm_left_iff {M : Type u_1} [] {a : Mˣ} {x : M} {y : M} :
SemiconjBy (a⁻¹) y x SemiconjBy (a) x y
theorem AddSemiconjBy.addUnits_val {M : Type u_1} [] {a : } {x : } {y : } (h : ) :
theorem SemiconjBy.units_val {M : Type u_1} [] {a : Mˣ} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) :
SemiconjBy a x y
theorem AddSemiconjBy.addUnits_of_val {M : Type u_1} [] {a : } {x : } {y : } (h : AddSemiconjBy a x y) :
theorem SemiconjBy.units_of_val {M : Type u_1} [] {a : Mˣ} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) :
@[simp]
theorem AddSemiconjBy.addUnits_val_iff {M : Type u_1} [] {a : } {x : } {y : } :
@[simp]
theorem SemiconjBy.units_val_iff {M : Type u_1} [] {a : Mˣ} {x : Mˣ} {y : Mˣ} :
SemiconjBy a x y SemiconjBy a x y
∀ (x : ), (∀ (n : ), motive ())(∀ (n : ), motive ())motive x
Equations
• =
Instances For
@[simp]
theorem AddSemiconjBy.addUnits_zsmul_right {M : Type u_1} [] {a : M} {x : } {y : } (h : AddSemiconjBy a x y) (m : ) :
AddSemiconjBy a (m x) (m y)
@[simp]
theorem SemiconjBy.units_zpow_right {M : Type u_1} [] {a : M} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) (m : ) :
SemiconjBy a (x ^ m) (y ^ m)
theorem AddUnits.mk_addSemiconjBy {M : Type u_1} [] (u : ) (x : M) :
AddSemiconjBy (u) x (u + x + (-u))

a semiconjugates x to a + x + -a.

theorem Units.mk_semiconjBy {M : Type u_1} [] (u : Mˣ) (x : M) :
SemiconjBy (u) x (u * x * u⁻¹)

a semiconjugates x to a * x * a⁻¹.

theorem Units.conj_pow {M : Type u_1} [] (u : Mˣ) (x : M) (n : ) :
(u * x * u⁻¹) ^ n = u * x ^ n * u⁻¹
theorem Units.conj_pow' {M : Type u_1} [] (u : Mˣ) (x : M) (n : ) :
(u⁻¹ * x * u) ^ n = u⁻¹ * x ^ n * u