# mathlibdocumentation

algebra.group.semiconj

# 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.

M → M → M → Prop

x is additive semiconjugate to y by a if a + x = y + a

def semiconj_by {M : Type u} [has_mul M] :
M → M → M → Prop

x is semiconjugate to y by a, if a * x = y * a.

Equations
• x y = (a * x = y * a)
theorem semiconj_by.eq {S : Type u} [has_mul S] {a x y : S} :
x ya * x = y * a

Equality behind semiconj_by a x y; useful for rewriting.

theorem add_semiconj_by.eq {S : Type u} [has_add S] {a x y : S} :
ya + x = y + a

@[simp]
theorem semiconj_by.mul_right {S : Type u} [semigroup S] {a x y x' y' : S} :
x y x' y' (x * x') (y * y')

If a semiconjugates x to y and x' to y', then it semiconjugates x * x' to y * y'.

theorem add_semiconj_by.add_right {S : Type u} {a x y x' y' : S} :
y x' y' (x + x') (y + y')

theorem semiconj_by.mul_left {S : Type u} [semigroup S] {a b x y z : S} :
y z x ysemiconj_by (a * b) x z

If both a and b semiconjugate x to y, then so does a * b.

theorem add_semiconj_by.add_left {S : Type u} {a b x y z : S} :
z yadd_semiconj_by (a + b) x z

@[simp]
theorem add_semiconj_by.zero_right {M : Type u} [add_monoid M] (a : M) :
0

@[simp]
theorem semiconj_by.one_right {M : Type u} [monoid M] (a : M) :
1 1

Any element semiconjugates 1 to 1.

@[simp]
theorem add_semiconj_by.zero_left {M : Type u} [add_monoid M] (x : M) :
x

@[simp]
theorem semiconj_by.one_left {M : Type u} [monoid M] (x : M) :
x x

One semiconjugates any element to itself.

theorem semiconj_by.units_inv_right {M : Type u} [monoid M] {a : M} {x y : units M} :
x y y⁻¹

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

theorem add_semiconj_by.units_neg_right {M : Type u} [add_monoid M] {a : M} {x y : add_units M} :
y (-x) (-y)

@[simp]
theorem add_semiconj_by.units_neg_right_iff {M : Type u} [add_monoid M] {a : M} {x y : add_units M} :
(-x) (-y) y

@[simp]
theorem semiconj_by.units_inv_right_iff {M : Type u} [monoid M] {a : M} {x y : units M} :

theorem add_semiconj_by.units_neg_symm_left {M : Type u} [add_monoid M] {a : add_units M} {x y : M} :
y y x

theorem semiconj_by.units_inv_symm_left {M : Type u} [monoid M] {a : units M} {x y : M} :
x y x

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

@[simp]
theorem semiconj_by.units_inv_symm_left_iff {M : Type u} [monoid M] {a : units M} {x y : M} :
x x y

@[simp]
theorem add_semiconj_by.units_neg_symm_left_iff {M : Type u} [add_monoid M] {a : add_units M} {x y : M} :
y x y

theorem semiconj_by.units_coe {M : Type u} [monoid M] {a x y : units M} :
x y y

y y

y y

theorem semiconj_by.units_of_coe {M : Type u} [monoid M] {a x y : units M} :
y x y

@[simp]
theorem semiconj_by.units_coe_iff {M : Type u} [monoid M] {a x y : units M} :
y x y

@[simp]
y y

@[simp]
theorem add_semiconj_by.neg_right_iff {G : Type u} [add_group G] {a x y : G} :
(-x) (-y) y

@[simp]
theorem semiconj_by.inv_right_iff {G : Type u} [group G] {a x y : G} :
y⁻¹ x y

theorem add_semiconj_by.neg_right {G : Type u} [add_group G] {a x y : G} :
y (-x) (-y)

theorem semiconj_by.inv_right {G : Type u} [group G] {a x y : G} :
x y y⁻¹

@[simp]
theorem semiconj_by.inv_symm_left_iff {G : Type u} [group G] {a x y : G} :
x x y

@[simp]
theorem add_semiconj_by.neg_symm_left_iff {G : Type u} [add_group G] {a x y : G} :
y x y

theorem add_semiconj_by.neg_symm_left {G : Type u} [add_group G] {a x y : G} :
y y x

theorem semiconj_by.inv_symm_left {G : Type u} [group G] {a x y : G} :
x y x

theorem add_semiconj_by.neg_neg_symm {G : Type u} [add_group G] {a x y : G} :
y (-y) (-x)

theorem semiconj_by.inv_inv_symm {G : Type u} [group G] {a x y : G} :
x y x⁻¹

theorem semiconj_by.inv_inv_symm_iff {G : Type u} [group G] {a x y : G} :
x⁻¹ x y

theorem add_semiconj_by.neg_neg_symm_iff {G : Type u} [add_group G] {a x y : G} :
(-y) (-x) y

theorem semiconj_by.conj_mk {G : Type u} [group G] (a x : G) :
x ((a * x) * a⁻¹)

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

theorem add_semiconj_by.conj_mk {G : Type u} [add_group G] (a x : G) :
(a + x + -a)

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