mathlib

ad0988b3 - docs(algebra/*): Add docstrings to additive lemmas (#12578)

docs(algebra/*): Add docstrings to additive lemmas (#12578) Many additive lemmas had no docstrings while their multiplicative counterparts had. This adds them in all files under `algebra`.