Lemmas about semiconjugate elements of a group #
@[simp]
theorem
AddSemiconjBy.neg_neg_symm_iff
{G : Type u_1}
[SubtractionMonoid G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
@[simp]
theorem
SemiconjBy.inv_inv_symm_iff
{G : Type u_1}
[DivisionMonoid G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
theorem
SemiconjBy.inv_inv_symm
{G : Type u_1}
[DivisionMonoid G]
{a : G}
{x : G}
{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 : G}
{x : G}
{y : G}
:
AddSemiconjBy a y x → AddSemiconjBy (-a) (-x) (-y)
@[simp]
theorem
AddSemiconjBy.neg_symm_left_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
@[simp]
theorem
SemiconjBy.inv_symm_left_iff
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
theorem
SemiconjBy.inv_symm_left
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{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 : G}
{x : G}
{y : G}
:
AddSemiconjBy a x y → AddSemiconjBy (-a) y x
@[simp]
theorem
AddSemiconjBy.neg_right_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{x : G}
{y : G}
:
AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
@[simp]
theorem
SemiconjBy.inv_right_iff
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{y : G}
:
SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
theorem
SemiconjBy.inv_right
{G : Type u_1}
[Group G]
{a : G}
{x : G}
{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 : G}
{x : G}
{y : G}
:
AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)