Theorems · Definition · general algebraic systems

DFinsupp.support

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

Set {i | f x ≠ 0} as a Finset.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

158 results in Mathlib

Foundations

Depth 75 from the axioms, rests on 1,380 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqZeroDecidable