Theorems · Definition · general algebraic systems

DFinsupp.neLocus

{α : Type u_1} →
  {N : α → Type u_2} →
    [DecidableEq α] →
      [(a : α) → DecidableEq (N a)] → [inst : (a : α) → Zero (N a)] → (Π₀ (a : α), N a) → (Π₀ (a : α), N a) → Finset α

Given two finitely supported functions f g : α →₀ N, Finsupp.neLocus f g is the Finset where f and g differ. This generalizes (f - g).support to situations without subtraction.

Defined in

Mathlib.Data.DFinsupp.NeLocus

Cited by

26 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqZero