Commit 2025-08-11 18:06 d678e826

View on Github →

chore: reformat to_additive docstrings to use docComment syntax (#28066) This PR reformats all to_additive docstrings in Mathlib to use docComment syntax instead of str syntax (except for the example docstring in to_additive's documentation, which will be reformatted when str syntax is deprecated). It does not deprecate str syntax; this is done in a subsequent PR (#28135).

Estimated changes