Lemmas about semiconjugate elements in a GroupWithZero.

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem SemiconjBy.inv_right₀ {G₀ : Type u_3} [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_3} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

theorem SemiconjBy.div_right {G₀ : Type u_3} [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')