Theorems · Definition · general algebraic systems

Finsupp.extendDomain

{α : Type u_1} → {M : Type u_12} → [inst : Zero M] → {P : α → Prop} → [DecidablePred P] → (Subtype P →₀ M) → α →₀ M

Extend the domain of a Finsupp by using 0 where P x does not hold.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

ZeroDecidablePred