Encodable and Countable instances for α →₀ β

In this file we provide instances for Encodable (α →₀ β) and Countable (α →₀ β).

instance instEncodableFinsupp {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] [Zero β] [(x : β) → Decidable (x ≠ 0)] : Encodable (α →₀ β)

Equations

• instEncodableFinsupp = Encodable.ofEquiv (Π₀ (x : α), β) finsuppEquivDFinsupp

instance instCountableFinsupp {α : Type u_1} {β : Type u_2} [Countable α] [Countable β] [Zero β] : Countable (α →₀ β)

Equations

• @instCountableFinsupp = @instCountableFinsupp.proof_1