Theorems · Theorem · general algebraic systems

sigmaFinsuppEquivDFinsupp_single

∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : Zero N] (a : (i : ι) × η i) (n : N),
  (sigmaFinsuppEquivDFinsupp fun₀ | a => n) = fun₀ | a.fst => fun₀ | a.snd => n

Defined in

Mathlib.Data.Finsupp.ToDFinsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqZero