AI for documentation

Stream: mathlib4

[Bolton Bailey]

@Matthew Ballard, you asked in the community meeting today what would happen if we asked Claude code to give us improved documentation.

I made #23964 by selecting 5 missing documentations in nolints.json and asking Cursor to document them. I would be curious to know what you or others think of what it provided. I have done one or two PRs trying to fix docs linter tech debt. Frankly , as far as I can tell, the documentation in this PR is fine, possibly better than what I would have produced if I tried to fix these myself. (I didn't change any of the text, I only fixed some line length violations, the AI it used under the hood is apparently Claude 3.5 sonnet).