Guidelines for tagging theorem as `protected`?

Stream: mathlib4

[Weiyi Wang]

Is there is a general guideline for when should one tag a new theorem as protected when contributing?

I tried following what existing code does, but sometimes it seems inconsistent. For example Asymptotic.IsEquivalent.mul is protected, but the similar theorem Asymptotic.IsBigO.mul is not

[Yury G. Kudryashov]

Generally, we're trying to protect theorems and definitions with common names. E.g., every lemma that has a version in _root_ or other commonly open namespace with the same name should be protected. This became more important in Lean 4, because in

theorem MyNamespace.my_theorem ...

it automatically opens MyNamespace, but this was not the case for Lean 3. So, many theorems that come from Lean 3 and live in rarely opened namespaces aren't protected.

[Yury G. Kudryashov]

PRs that add protected to lemmas are welcome!

[Weiyi Wang]

I see. So in the example I linked, it is because mul is the name of the operator itself, and there are other closely related namespace like Tendsto that has mul, so it is desirable to have protected. I'll PR missing ones that I find

[Yury G. Kudryashov]

On the one hand, I can't easily imagine a situation when both Asymptotics.IsBigO and Filter.Tendsto are open. OTOH, if this will occur, then the error message may be very strange.