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)
abbrev AddSemiconjBy.zsmul_right.match_1 (motive : Prop) :
∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
Equations
  • =
Instances For
    @[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