Theorems · Definition · general algebraic systems

Finsupp.restrictSupportEquiv

{α : Type u_1} → (s : Set α) → (M : Type u_12) → [inst : AddCommMonoid M] → { f // ↑f.support ⊆ s } ≃ (↑s →₀ M)

Given an AddCommMonoid M and s : Set α, restrictSupportEquiv s M is the Equiv between the subtype of finitely supported functions with support contained in s and the type of finitely supported functions from s.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddCommMonoid