no goals
α : Type ?u.23833
M₀ : Type ?u.23836
G₀ : Type u_1
M₀' : Type ?u.23842
G₀' : Type ?u.23845
F : Type ?u.23848
F' : Type ?u.23851
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / 0 = 0
rw [div_eq_mul_inv, inv_zero, mul_zero]