chore(Algebra/BigOperators): fix misnamed lemma

[b-mehta]

The to_additive version of this lemma was incorrectly named in Lean 3, which seemingly led to some confusion in porting

---

[bors[bot]]

:v: b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[b-mehta]

This doesn't just fix a name; it adds a missing lemma, right?

No - this isn't adding any new lemmas. Or more specifically, there were two lemmas with different content but the same name, so one of them was inaccessible; this PR fixes the name of the latter so it becomes accessible, but the lemma and its proof were in mathlib all along

[eric-wieser]

Doesn't this add a new Finest.sum_eq_zero_iff_of_nonpos lemma?

[eric-wieser]

I don't think the lemma you're thinking of was inaccessible; it was never generated so didn't exist at all.

[grunweg]

Coming here from issue triage: what's the current state of this PR (except for the merge conflict)?

[github-actions[bot]]

PR summary 582a78bf9f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[b-mehta]

The changes in the original PR here were bundled in with #9371, and incorporated there.