Bhavik Mehta

[The man, the legend. Let's do it.](https://ncatlab.org/nlab/show/subobject+classifier#johnstones_exercise)

chore(Algebra/BigOperators): fix misnamed lemma

5

The to_additive version of this lemma was incorrectly named in Lean 3, which seemingly led to some confusion in porting --- [](https://gitpod.io/from-referrer/)