Theorems · Definition · general algebraic systems

Finsupp.onFinset

{α : Type u_1} → {M : Type u_4} → [inst : Zero M] → (s : Finset α) → (f : α → M) → (∀ (a : α), f a ≠ 0 → a ∈ s) → α →₀ M

Finsupp.onFinset s f hf is the finsupp function representing f restricted to the finset s. The function must be 0 outside of s. Use this when the set needs to be filtered anyways, otherwise a better set representation is often available.

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

20 results in Mathlib

Foundations

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

Assumes

Zero