Theorems · Theorem · general algebraic systems

Finsupp.extendDomain_single

∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (a : Subtype P) (m : M),
  (fun₀ | a => m).extendDomain = fun₀ | ↑a => m

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

ZeroDecidablePred