Lemmas about semiconjugate elements of a group

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

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

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.

theorem AddSemiconjBy.neg_neg_symm {G : Type u_1} [SubtractionMonoid G] {a x y : G} : AddSemiconjBy a y x → AddSemiconjBy (-a) (-x) (-y)

Alias of the reverse direction of AddSemiconjBy.neg_neg_symm_iff.

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

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

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.

theorem AddSemiconjBy.neg_symm_left {G : Type u_1} [AddGroup G] {a x y : G} : AddSemiconjBy a x y → AddSemiconjBy (-a) y x

Alias of the reverse direction of AddSemiconjBy.neg_symm_left_iff.

@[simp]

theorem SemiconjBy.inv_right_iff {G : Type u_1} [Group G] {a x y : G} : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

@[simp]

theorem AddSemiconjBy.neg_right_iff {G : Type u_1} [AddGroup G] {a x y : G} : AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y

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.

theorem AddSemiconjBy.neg_right {G : Type u_1} [AddGroup G] {a x y : G} : AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)

Alias of the reverse direction of AddSemiconjBy.neg_right_iff.

@[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)

@[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)

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

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