Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-06 08:37 2bdeda9c

View on Github →

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.

Estimated changes