Documentation

Mathlib.Algebra.Group.Semiconj.Basic

Lemmas about semiconjugate elements of a semigroup #

@[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 AddSemiconjBy.neg_neg_symm {G : Type u_1} [SubtractionMonoid G] {a : G} {x : G} {y : G} :
AddSemiconjBy a x yAddSemiconjBy (-a) (-y) (-x)
theorem SemiconjBy.inv_inv_symm {G : Type u_1} [DivisionMonoid G] {a : G} {x : G} {y : G} :