no goals
α : Type ?u.23516
M₀ : Type ?u.23519
G₀ : Type u_1
M₀' : Type ?u.23525
G₀' : Type ?u.23528
F : Type ?u.23531
F' : Type ?u.23534
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ 0 / a = 0
rw [div_eq_mul_inv, zero_mul]