# Lemmas about semiconjugate elements of a group #

source
@[simp]
theorem SemiconjBy.inv_inv_symm_iff {G : Type u_1} [DivisionMonoid G] {a x y : G} :
SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
source
@[simp]
theorem AddSemiconjBy.neg_neg_symm_iff {G : Type u_1} [SubtractionMonoid G] {a x y : G} :
AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
source
theorem SemiconjBy.inv_inv_symm {G : Type u_1} [DivisionMonoid G] {a x y : G} :
SemiconjBy a y x → SemiconjBy a⁻¹ x⁻¹ y⁻¹

Alias of the reverse direction of `SemiconjBy.inv_inv_symm_iff`.

source
theorem AddSemiconjBy.neg_neg_symm {G : Type u_1} [SubtractionMonoid G] {a x y : G} :
AddSemiconjBy a y x → AddSemiconjBy (-a) (-x) (-y)
source
@[simp]
theorem SemiconjBy.inv_symm_left_iff {G : Type u_1} [Group G] {a x y : G} :
SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
source
@[simp]
theorem AddSemiconjBy.neg_symm_left_iff {G : Type u_1} [AddGroup G] {a x y : G} :
AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
source
theorem SemiconjBy.inv_symm_left {G : Type u_1} [Group G] {a x y : G} :
SemiconjBy a x y → SemiconjBy a⁻¹ y x

Alias of the reverse direction of `SemiconjBy.inv_symm_left_iff`.

source
theorem AddSemiconjBy.neg_symm_left {G : Type u_1} [AddGroup G] {a x y : G} :
AddSemiconjBy a x y → AddSemiconjBy (-a) y x
source
@[simp]
theorem SemiconjBy.inv_right_iff {G : Type u_1} [Group G] {a x y : G} :
SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
source
@[simp]
theorem AddSemiconjBy.neg_right_iff {G : Type u_1} [AddGroup G] {a x y : G} :
AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
source
theorem SemiconjBy.inv_right {G : Type u_1} [Group G] {a x y : G} :
SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹

Alias of the reverse direction of `SemiconjBy.inv_right_iff`.

source
theorem AddSemiconjBy.neg_right {G : Type u_1} [AddGroup G] {a x y : G} :
AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)
source
@[simp]
theorem SemiconjBy.zpow_right {G : Type u_1} [Group G] {a x y : G} (h : SemiconjBy a x y) (m : ℤ) :
SemiconjBy a (x ^ m) (y ^ m)
source
@[simp]
theorem AddSemiconjBy.zsmul_right {G : Type u_1} [AddGroup G] {a x y : G} (h : AddSemiconjBy a x y) (m : ℤ) :
AddSemiconjBy a (m • x) (m • y)
source
theorem SemiconjBy.eq_one_iff {G : Type u_1} [Group G] (a : G) {x y : G} (h : SemiconjBy a x y) :
x = 1 ↔ y = 1
source
theorem AddSemiconjBy.eq_zero_iff {G : Type u_1} [AddGroup G] (a : G) {x y : G} (h : AddSemiconjBy a x y) :
x = 0 ↔ y = 0