Locus of unequal values of finitely supported functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
α N be two Types, assume that
N has a
0 and let
f g : α →₀ N be finitely supported
Main definition #
In the case in which
N is an additive group,
finsupp.ne_locus f g coincides with
finsupp.support (f - g).
Given two finitely supported functions
f g : α →₀ N,
finsupp.ne_locus f g is the
g differ. This generalizes
(f - g).support to situations without subtraction.