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