Theorems · Definition · general algebraic systems

Finsupp.equivMapDomain

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

Given f : α ≃ β, we can map l : α →₀ M to equivMapDomain f l : β →₀ M (computably) by mapping the support forwards and the function backwards.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

35 results in Mathlib

Foundations

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

Assumes

Zero