Theorems · Theorem · general algebraic systems

DFinsupp.toFinsupp_single

∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)] (i : ι)
  (m : M), (fun₀ | i => m).toFinsupp = fun₀ | i => m

Defined in

Mathlib.Data.Finsupp.ToDFinsupp

Cited by

8 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroDecidable