mathlib documentation

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.

def add_semiconj_by {M : Type u} [has_add M] :
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
theorem semiconj_by.eq {S : Type u} [has_mul S] {a x y : S} :
semiconj_by a 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} :
add_semiconj_by a x ya + x = y + a

@[simp]
theorem semiconj_by.mul_right {S : Type u} [semigroup S] {a x y x' y' : S} :
semiconj_by a x ysemiconj_by a x' y'semiconj_by a (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} [add_semigroup S] {a x y x' y' : S} :
add_semiconj_by a x yadd_semiconj_by a x' y'add_semiconj_by a (x + x') (y + y')

theorem semiconj_by.mul_left {S : Type u} [semigroup S] {a b x y z : S} :
semiconj_by a y zsemiconj_by b 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} [add_semigroup S] {a b x y z : S} :
add_semiconj_by a y zadd_semiconj_by b x yadd_semiconj_by (a + b) x z

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

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

Any element semiconjugates 1 to 1.

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

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

One semiconjugates any element to itself.

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

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} :

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

@[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} :

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

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} :

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

theorem semiconj_by.conj_mk {G : Type u} [group G] (a x : G) :
semiconj_by a 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) :
add_semiconj_by a x (a + x + -a)

theorem add_units.mk_semiconj_by {M : Type u} [add_monoid M] (u : add_units M) (x : M) :

theorem units.mk_semiconj_by {M : Type u} [monoid M] (u : units M) (x : M) :
semiconj_by u x (((u) * x) * u⁻¹)

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