Technical debt: docstrings

[kbuzzard]

https://github.com/kbuzzard/ClassFieldTheory/blob/main/scripts/nolints.json indicates that there are many docstrings which need to be written in order to conform to Mathlib's linter standards.