# Lemmas about semiconjugate elements in a `GroupWithZero`. #

source
@[simp]
theorem SemiconjBy.zero_right {G₀ : Type u_1} [MulZeroClass G₀] (a : G₀) :
SemiconjBy a 0 0
source
@[simp]
theorem SemiconjBy.zero_left {G₀ : Type u_1} [MulZeroClass G₀] (x y : G₀) :
SemiconjBy 0 x y
source
@[simp]
theorem SemiconjBy.inv_symm_left_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a x y : G₀} :
SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x
source
theorem SemiconjBy.inv_symm_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a x y : G₀} (h : SemiconjBy a x y) :
SemiconjBy a⁻¹ y x
source
theorem SemiconjBy.inv_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a x y : G₀} (h : SemiconjBy a x y) :
SemiconjBy a x⁻¹ y⁻¹
source
@[simp]
theorem SemiconjBy.inv_right_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a x y : G₀} :
SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
source
theorem SemiconjBy.div_right {G₀ : Type u_1} [GroupWithZero G₀] {a x y x' y' : G₀} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
SemiconjBy a (x / x') (y / y')
source
theorem SemiconjBy.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a x y : G₀} (h : SemiconjBy a x y) (m : ℤ) :
SemiconjBy a (x ^ m) (y ^ m)
source
theorem Commute.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a b : G₀} (h : Commute a b) (m : ℤ) :
Commute a (b ^ m)
source
theorem Commute.zpow_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a b : G₀} (h : Commute a b) (m : ℤ) :
Commute (a ^ m) b
source
theorem Commute.zpow_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] {a b : G₀} (h : Commute a b) (m n : ℤ) :
Commute (a ^ m) (b ^ n)
source
theorem Commute.zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) :
Commute (a ^ n) a
source
theorem Commute.self_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) :
Commute a (a ^ n)
source
theorem Commute.zpow_zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (m n : ℤ) :
Commute (a ^ m) (a ^ n)