Commit 2026-09-11 01:27 04c9bc87

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