Theorems · Definition · general algebraic systems

Finsupp.embDomain

{α : Type u_1} → {β : Type u_2} → {M : Type u_4} → [inst : Zero M] → (α ↪ β) → (α →₀ M) → β →₀ M

Given f : α ↪ β and v : α →₀ M, Finsupp.embDomain f v : β →₀ M is the finitely supported function whose value at f a : β is v a. For a b : β outside the range of f, it is zero.

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

69 results in Mathlib

Foundations

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

Assumes

Zero