Commit 2025-08-29 21:26 f55227af

chore(Data): make arguments consistent for single_eq_of_ne (#29006)

• Swap the direction of the hypothesis in Finsupp.single_eq_of_ne and Dfinsupp.single_eq_of_ne to match Pi.single_eq_of_ne and *.apply_eq_of_ne
• Move existing Finsupp.single_eq_of_ne to Finsupp.single_eq_of_ne' to aid simp, in line with Pi.single_eq_of_ne'
• Swap the hypothesis direction in DirectSum.of_eq_of_ne and Polynomial.coeff_monomial_of_ne to match the above This change means that, in order to prove that (fun₀ | i => x) j = 0, you supply j ≠ i rather than i ≠ j by default. See Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Inconsistent.20hypothesis.20convention.20in.20.60Finsupp.60 The cutoff for which declarations I edited and which I didn't is somewhat arbitrary. For now, I only changed declarations which obviously had the meaning of evaluating a delta function f i at an index j.