Theorems · Definition · general algebraic systems

DFinsupp.equivFunOnFintype

{ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [Fintype ι] → (Π₀ (i : ι), β i) ≃ ((i : ι) → β i)

Given Fintype ι, equivFunOnFintype is the Equiv between Π₀ i, β i and Π i, β i. (All dependent functions on a finite type are finitely supported.)

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

11 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ZeroFintype