Theorem: Finset.card_mulStab_dvd_card (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab.card ∣ s.card
Tactic:
simpa only [mul_mulStab] using s.card_mulStab_dvd_card_mul_mulStab s
State after:
no goals