Commit 2026-08-10 16:29 bf0fb2be

chore: add missing to_additive docstrings in GroupTheory (#41641) Adds the missing additive doc-strings (multiplicative side has a hand-written doc-string, additive side did not) across 17 file(s) in GroupTheory. The additive doc-strings are simple-minded translations of the multiplicative ones, with referenced lemma names replaced by their to_additive counterparts. These gaps were found by an environment linter that pairs each declaration with its to_additive counterpart and checks that both or neither is documented. 🤖 Generated with Claude Code