ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ ∏ i in f.support, card (↑f i) = prod f fun i => ↑(card (↑f i))
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
rw [pi, card_finsupp]
no goals
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ ∏ i in f.support, card (↑f i) = prod f fun i => ↑(card (↑f i))
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
no goals
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
i : ι
x✝ : i ∈ f.support
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
simp only [Pi.nat_apply, Nat.cast_id]