Documentation

Mathlib.Algebra.Group.Semiconj.Basic

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} :
@[simp]
theorem SemiconjBy.inv_inv_symm_iff {G : Type u_1} [DivisionMonoid G] {a : G} {x : G} {y : G} :
theorem SemiconjBy.inv_inv_symm {G : Type u_1} [DivisionMonoid G] {a : G} {x : G} {y : G} :

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 xAddSemiconjBy (-a) (-x) (-y)
@[simp]
theorem AddSemiconjBy.neg_symm_left_iff {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} :
@[simp]
theorem SemiconjBy.inv_symm_left_iff {G : Type u_1} [Group G] {a : G} {x : G} {y : G} :
theorem SemiconjBy.inv_symm_left {G : Type u_1} [Group G] {a : G} {x : G} {y : G} :
SemiconjBy a x ySemiconjBy 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 yAddSemiconjBy (-a) y x
@[simp]
theorem AddSemiconjBy.neg_right_iff {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} :
@[simp]
theorem SemiconjBy.inv_right_iff {G : Type u_1} [Group G] {a : G} {x : G} {y : G} :
theorem SemiconjBy.inv_right {G : Type u_1} [Group G] {a : G} {x : G} {y : G} :

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 yAddSemiconjBy a (-x) (-y)
@[simp]
theorem AddSemiconjBy.zsmul_right {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} (h : AddSemiconjBy a x y) (m : ) :
AddSemiconjBy a (m x) (m y)
@[simp]
theorem SemiconjBy.zpow_right {G : Type u_1} [Group G] {a : G} {x : G} {y : G} (h : SemiconjBy a x y) (m : ) :
SemiconjBy a (x ^ m) (y ^ m)
theorem AddSemiconjBy.eq_zero_iff {G : Type u_1} [AddGroup G] (a : G) {x : G} {y : G} (h : AddSemiconjBy a x y) :
x = 0 y = 0
theorem SemiconjBy.eq_one_iff {G : Type u_1} [Group G] (a : G) {x : G} {y : G} (h : SemiconjBy a x y) :
x = 1 y = 1