no goals
F : Type ?u.652865
α : Type u_1
β : Type ?u.652871
γ : Type ?u.652874
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ s / 0 ⊆ 0
simp [subset_iff, mem_div]