feat(data/finsupp/ne_locus): new file with finsupp.ne_locus (#16091)
feat(data/finsupp/ne_locus): new file with finsupp.ne_locus (#16091)

`finsupp.ne_locus` for finitely supported functions.

Let `α N` be two Types, and assume that `N` has a `0` and let `f g : α →₀ N` be finitely supported
functions.

This PR defines `finsupp.ne_locus f g : finset α`, the finite subset of `α` where `f` and `g` differ.

In the case in which `N` is an additive group, `finsupp.ne_locus f g` coincides with `finsupp.support (f - g)`.

This is the initial segment of #16026, that continues with the definition of witnesses.

[Zulip discussion for the choice of name](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60diff.60.20vs.20.60ne_locus.60)
[Zulip discussion for the actual PR](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2316091.20.60ne_locus.60)





leanprover-community/mathlib,leanprover-community/mathlib