mathlib3

a19f6c6f - doc(algebra/group/to_additive): `to_additive` and docstring interaction (#12476)