feat(naming): document the ₀ suffix convention

[YaelDillies]

Many lemmas about GroupWithZero have an analogous Group lemma (and similarly for weaker/stronger typeclasses). In cases where the former name doesn't mention zero, it is prone to conflict with the latter. Historically, this was dealt with by priming the latter, which created a lot of primed lemmas and meant that the AddMonoid lemma name couldn't be inferred from the Monoid one automatically by to_additive.

A while ago, there was a push to unprime the Group lemmas and add the suffix ₀ to the GroupWithZero ones, see leanprover-community/mathlib3#9424 among others. Unfortunately that new naming convention was never recorded and wasn't applied everywhere, meaning it wasn't subsequently consistently followed.

This PR records the convention.

Pros of the convention:

• to_additive guesses the correct name for the AddGroup lemmas
• We need fewer primes overall

Cons of the convention

• The GroupWithZero lemma is sometimes used more than the Group one, but gets a longer name
• It is harder to type ₀ than ', in particular in the docs. This could be fixed by making 0 search for ₀.

Zulip

[grunweg]

Thanks for documenting this! I have one question about the example you're giving.

[grunweg]

Also: is there any evidence of this convention being discussed previously? I trust your memory, but having an explicit source to consult (also down the line) will be very very helpful.

[YaelDillies]

Here is the PR which I believe introduced the naming convention: leanprover-community/mathlib3#9424

[b-mehta]

I feel it's important to mention here that the proposed change here is explicitly contradicted by existing documentation (eg https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Group/Defs.html#ContinuousDiv or https://github.com/leanprover-community/mathlib4/blob/4176265817544b3530eca07e02a704b0316f2ab8/Mathlib/Data/Nat/Cast/Basic.lean#L97 or https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean#L21), and followed the minority of the time in mathlib. As such, this PR isn't documenting a convention, but essentially proposing a new one, which doesn't reflect existing practice.
Note that in the three examples I link above, there is an existing convention, which is that the unprimed versions are used for MonoidWithZero-like things, and primed versions are used for Monoid-like things to avoid ambiguity, which has the additional benefit that for the (overwhelmingly common) case of rings, the name is shorter.

[YaelDillies]

Quoting @kim-em in the PR I linked to above:

We currently have lots of lemmas for group_with_zero that already have a corresponding lemma for group. We've dealt with name collisions so far just by adding a prime.
In part this is out of desire to reduce our overuse of primes in mathlib names (putting the burden on users to know names, rather than relying on naming conventions).

I personally believe that the extra character for the common case is worth it to achieve consistency and clarity (remember that there are many other reasons to prime a name).

[YaelDillies]

Also note that I can't remove the awaiting-author label here, so I am not sure what its use is

[grunweg]

Oh, I wasn't aware of that.
@bryangingechen How much work would it be to add the -awaiting-author workflow?

[b-mehta]

I personally believe that the extra character for the common case is worth it to achieve consistency and clarity (remember that there are many other reasons to prime a name).

Sure, I am not arguing against your change, but instead trying to make it clear that this is a change to the (both de jure and de facto) convention, not just "documenting existing practice".

[grunweg]

So, with my "process nerd" hat on, this sounds like a case for additional discussion.
@YaelDillies Would you like to open a thread in mathlib reviewers, arguing for your reading? I think consistency is useful here, but that can and will only work if there's consensus in favour of this.
Even if this was decided ages ago (it was before my mathlib time, so I won't comment on the facts), sometimes decisions deserve being revisited, if only to be affirmed.

[YaelDillies]

See https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/The.20.E2.82.80.20suffix/with/604871388

[YaelDillies]

-awaiting-author

[YaelDillies]

Yep, no, doesn't work 😅

[JovanGerb]

I think you might have meant to say that lemmas in series 1 and 3 can clash? E.g. mul_le_mul_left vs mul_le_mul_of_nonneg_left

[grunweg]

Thanks! Finally, can you update the PR description to reference the Zulip discussion (this I will insist on) and (would be nice, but optional) explain the trade-off that we make here (e.g. around linkifiers, unicode in identifiers, to_additive support versus longer names)?

[YaelDillies]

How about now?

[grunweg]

Looks good. I changed one word to be unambiguous.
-awaiting-author