mathlib3

5c2088ed - feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)

feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330) many of our `nolint.txt` entires are due to code of this shape: @[to_additive add_foo] lemma foo := .. /- no docstring -/ alias foo <- bar attribute [to_additive add_bar] bar where now `bar` has a docstring (from `alias`), but `bar_add` does not. This PR makes `to_additive` detect that `bar` is an alias, and unless an explicit docstring is passed to `to_additive`, creates an “alias of add_foo” docstring.