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).