mathlib3

5ad44a90 - 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)