chore(TwoSidedIdeal/Basic): fix docs string

[jjaassoonn]

After being delegated, I forgot to apply the suggestions from #13902 by @jcommelin ....

---

[github-actions[bot]]

PR summary d0573644a5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

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>

[grunweg]

Thanks for following up! I have just one tiny question; would maintainer merge with that addressed. Did you think about this part of jcommelin's comment?

Then you can use it in theproofs of sub_mem and nsmul_mem etc [...] this isn't very important

[jjaassoonn]

Thanks for following up! I have just one tiny question; would maintainer merge with that addressed. Did you think about this part of jcommelin's comment?

Then you can use it in theproofs of sub_mem and nsmul_mem etc [...] this isn't very important

Thanks for pointing this out. I have applied this suggestion as well!

[grunweg]

Thanks! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style