no goals
α : Type ?u.28276
M₀ : Type ?u.28279
G₀ : Type u_1
M₀' : Type ?u.28285
G₀' : Type ?u.28288
F : Type ?u.28291
F' : Type ?u.28294
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a⁻¹ = 0 ↔ a = 0
rw [inv_eq_iff_eq_inv, inv_zero]