mathlib
2bdeda9c - doc(number_theory/*): provide docstrings for basic and dioph (#6063)

Commit
4 years ago
doc(number_theory/*): provide docstrings for basic and dioph (#6063) The main purpose of this PR is to provide docstrings for the two remaining files without docstring in number_theory, basic and dioph. Furthermore, lines are split in other files, so that there should be no number_theory entries in the style_exceptions file. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Parents
Loading