[GOAL]
α : Type ?u.651
β : Type ?u.647
inst✝² : Countable α
inst✝¹ : Countable β
inst✝ : Zero β
⊢ Countable (α →₀ β)
[PROOFSTEP]
classical exact .of_equiv _ finsuppEquivDFinsupp.symm
[GOAL]
α : Type ?u.651
β : Type ?u.647
inst✝² : Countable α
inst✝¹ : Countable β
inst✝ : Zero β
⊢ Countable (α →₀ β)
[PROOFSTEP]
exact .of_equiv _ finsuppEquivDFinsupp.symm
