Theorem: Finset.mulImpact_empty (LeanCamCombi/Impact.lean)

State before:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Mul α
n✝ n : ℕ
⊢ ∅.mulImpact n = 0
Tactic:
simp [mulImpact]
State after:
no goals