no goals
α : Type ?u.19455
M₀ : Type ?u.19458
G₀ : Type u_1
M₀' : Type ?u.19464
G₀' : Type ?u.19467
F : Type ?u.19470
F' : Type ?u.19473
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
⊢ a / b = 0 ↔ a = 0 ∨ b = 0
simp [div_eq_mul_inv]