[Merged by Bors] - chore: Improved nth_rewrite and nth_rw docstrings

[Shreyas4991]

Zulip thread of discussion

---

[github-actions]

PR summary 7952c9c003

Import changes

No significant changes to the import graph

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[rwst]

The whole change is much welcome. As a new user I can understand the text, and Grammarl y only complains about "afterward(s)".

[Shreyas4991]

That's some Americanism by grammarly. "Afterwards" is definitely correct in English.

See : https://dictionary.cambridge.org/thesaurus/articles/afterwards

[Ruben-VandeVelde]

Thanks!

[j-loreaux]

LGTM. Another maintainer can review the above unresolved conversations to see if they feel anything should be done. Make sure to wait for CI (probably doesn't matter since it's only docstrings, but still).

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[Shreyas4991]

what is a maintainer merge and given that the bot says it is already on some merge queue, I am not sure how I wait for CI.

[Vierkantor]

@semorrison I'm okay either way, applying your suggestion to copy the docs or not. Do you want to make the final decision?

[j-loreaux]

@Shreyas4991 a maintainer merge is when a reviewer places a PR on a queue (really just a thread in a private channel on Zulip) for a maintainer to look at and potentially merge. Sometimes maintainers themselves use this queue so that they can get approval from another maintainer, as I have done here. You can still wait for CI as normal, but unlike delegation, a maintainer merge does not give anyone the authority to merge (other than maintainers themselves, but they already had such authority). Note: my reference to CI was for the maintainer so that they didn't think it was already fully prepared for merging.

[joneugster]

I resolved the open suggestion, since I don't consider them necessary and other reviewers didn't either.

I read through the text again and it's really clear. Left some comma suggestions, but I think it should be merged with or without them

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style