Theorems · Definition · general algebraic systems

Finsupp.equivFunOnFinite

{α : Type u_1} → {M : Type u_4} → [inst : Zero M] → [Finite α] → (α →₀ M) ≃ (α → M)

Given Finite α, equivFunOnFinite is the Equiv between α →₀ β and α → β. (All functions on a finite type are finitely supported.)

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

50 results in Mathlib

Foundations

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

Assumes

ZeroFinite