α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = ∑ t in powerset s, (∏ a_1 in t, a) * ∏ a in s \ t, b
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = (a + b) ^ card s
rw [← prod_const, prod_add]
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s t : Finset α
ht : t ∈ powerset s
⊢ a ^ card t * b ^ (card s - card t) = (∏ a_1 in t, a) * ∏ a in s \ t, b
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = ∑ t in powerset s, (∏ a_1 in t, a) * ∏ a in s \ t, b
refine' Finset.sum_congr rfl fun t ht => _
no goals
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s t : Finset α
ht : t ∈ powerset s
⊢ a ^ card t * b ^ (card s - card t) = (∏ a_1 in t, a) * ∏ a in s \ t, b
rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]