Conjugacy in a group with zero

@[simp]

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