Theorems · Theorem · general algebraic systems

DFinsupp.mem_support_toFun

∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι), i ∈ f.support ↔ f i ≠ 0

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroDecidable