PR related to big O notation

Stream: PrimeNumberTheorem+

[Johan Commelin]

Can I solicit a PR review from people working on this project?

feat: dot notation for IsTheta.add_isLittleO, and add_commed variants #10386 (+19/-3)

In particular, I would like to hear suggestions for the names, by people who use this part of the library.

[Alex Kontorovich]

I think it looks good to me. Added a review.