R : Type ?u.208984
α : Type u_1
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in range (card x + 1), Nat.choose (card x) m • (-1) ^ m = if x = ∅ then 1 else 0
R : Type ?u.208984
α : Type u_1
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in powerset x, (-1) ^ card m = if x = ∅ then 1 else 0
rw [sum_powerset_apply_card]
no goals
R : Type ?u.208984
α : Type u_1
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in range (card x + 1), Nat.choose (card x) m • (-1) ^ m = if x = ∅ then 1 else 0
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]