Conjugacy in a group with zero

@[simp]

theorem GroupWithZero.isConj_iff₀ {α : Type u_1} [GroupWithZero α] {a b : α} : IsConj a b ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b

theorem GroupWithZero.conj_pow₀ {α : Type u_1} [GroupWithZero α] {s : ℕ} {a d : α} (ha : a ≠ 0) : (a⁻¹ * d * a) ^ s = a⁻¹ * d ^ s * a