Theorems · Definition · general algebraic systems

Finsupp.comapDomain

{α : Type u_1} →
  {β : Type u_2} →
    {M : Type u_5} → [inst : Zero M] → (f : α → β) → (l : β →₀ M) → Set.InjOn f (f ⁻¹' ↑l.support) → α →₀ M

Given f : α → β, l : β →₀ M and a proof hf that f is injective on the preimage of l.support, comapDomain f l hf is the finitely supported function from α to M given by composing l with f.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

40 results in Mathlib

Foundations

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

Assumes

Zero