mathlib
c42cff11 - doc(deprecated/*): all deprecated files now lint (#14233)

Commit

3 years ago

doc(deprecated/*): all deprecated files now lint (#14233) I am happy to remove some nolints for you.

Author

kbuzzard

Parents