Lemmas about semiconjugate elements in a GroupWithZero.

@[simp]

theorem SemiconjBy.zero_right {G₀ : Type u_1} [MulZeroClass G₀] (a : G₀) : SemiconjBy a 0 0

@[simp]

theorem SemiconjBy.zero_left {G₀ : Type u_1} [MulZeroClass G₀] (x : G₀) (y : G₀) : SemiconjBy 0 x y

@[simp]

theorem SemiconjBy.inv_symm_left_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} : SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

theorem SemiconjBy.inv_symm_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) : SemiconjBy a⁻¹ y x

theorem SemiconjBy.inv_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) : SemiconjBy a x⁻¹ y⁻¹

@[simp]

theorem SemiconjBy.inv_right_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

theorem SemiconjBy.div_right {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} {x' : G₀} {y' : G₀} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x / x') (y / y')

theorem SemiconjBy.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) (m : ℤ) : SemiconjBy a (x ^ m) (y ^ m)

theorem Commute.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) : Commute a (b ^ m)

theorem Commute.zpow_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) : Commute (a ^ m) b

theorem Commute.zpow_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) (n : ℤ) : Commute (a ^ m) (b ^ n)

theorem Commute.zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : Commute (a ^ n) a

theorem Commute.self_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : Commute a (a ^ n)

theorem Commute.zpow_zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (m : ℤ) (n : ℤ) : Commute (a ^ m) (a ^ n)