Encodable and Countable instances for Π₀ i, α i

In this file we provide instances for Encodable (Π₀ i, α i) and Countable (Π₀ i, α i).

@[implicit_reducible]

instance instEncodableDFinsuppOfDecidableNeOfNat {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Encodable ι] [(i : ι) → Encodable (α i)] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : Encodable (Π₀ (i : ι), α i)

instance instCountableDFinsupp {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Countable ι] [∀ (i : ι), Countable (α i)] : Countable (Π₀ (i : ι), α i)