Theorems · Definition · general algebraic systems

DFinsupp.update

{ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → [DecidableEq ι] → (Π₀ (i : ι), β i) → (i : ι) → β i → Π₀ (i : ι), β i

Replace the value of a Π₀ i, β i at a given point i : ι by a given value b : β i. If b = 0, this amounts to removing i from the support. Otherwise, i is added to it. This is the (dependent) finitely-supported version of Function.update.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

8 results in Mathlib

Foundations

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

Assumes

ZeroDecidableEq