Commit 2022-03-08 08:30 47182da5
View on Github →feat(algebra/group/to_additive): add to_additive doc string linter (#12487)
it is an easy mistake to add a docstring to a lemma with to_additive
without also passing a string to to_additive. This linter checks for
that, and suggests to add a doc string when needed.