Theorems · Definition · general algebraic systems

Finsupp.neLocus

{α : Type u_1} → {N : Type u_3} → [DecidableEq α] → [DecidableEq N] → [inst : Zero N] → (α →₀ N) → (α →₀ N) → 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.Finsupp.NeLocus

Cited by

24 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqZero