mathlib3

22e33e9d - refactor(data/finsupp/ne_locus): Match `dist` API (#17036)

refactor(data/finsupp/ne_locus): Match `dist` API (#17036) Rename `ne_locus` lemmas so they match the `dist` one. This is the name of them both being binary functions `f` such that `f a b = g (a - b)` for some `g`.