Skip to content

chore: add missing to_additive docstrings in Combinatorics and Dynamics#41645

Open
adomani wants to merge 3 commits into
leanprover-community:masterfrom
adomani:to_additive-docs-combinatorics-dynamics
Open

chore: add missing to_additive docstrings in Combinatorics and Dynamics#41645
adomani wants to merge 3 commits into
leanprover-community:masterfrom
adomani:to_additive-docs-combinatorics-dynamics

chore: wrap over-length `to_additive` docstring line

53772c3
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jul 13, 2026 in 1m 38s