Commit 2026-08-07 03:47 daa38bd5

chore: add missing to_additive docstrings in Combinatorics and Dynamics (#41645) Adds the missing additive doc-strings (multiplicative side has a hand-written doc-string, additive side did not) across 5 file(s) in Combinatorics and Dynamics. 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