prodZeroRing vs prodUnique

Stream: mathlib4

[Lukas Miaskiwskyi]

As discussed in #9105, there's a slight difference in naming & assumptions for lemmas of the form A ≃ A × B for when B is the zero ring/zero module/singleton; we have docs4#RingEquiv.prodZeroRing for Ring, but e.g. docs4#Equiv.prodUnique for general Type and docs4#AddEquiv.prodUnique for Monoid. The former also assumes [Subsingleton B], the latter (necessarily) [Unique B].

I'm wondering what's the nicest way to treat these. Arguably, these could all just use [Unique B] and be named prodUnique -- then again, personally, I was first looking for something like prodZero or prodZeroModule when I started hunting these down, so the prodZeroRing approach may be more intuitive. Any thoughts?

If nothing else, I'll make them refer to one another in the PR.

[Yaël Dillies]

I'm slightly in favor of prodUnique

[Eric Wieser]

The nice thing about assuming [Subsingleton R] instead of [Unique R] is that the equiv is defeq to 0 in certain place, whereas for Unique it's defeq to default which may only be Prop-eq to 0.

[Yaël Dillies]

I think that's orthogonal to the name?

[Eric Wieser]

Not entirely, using unique in a name is slightly harder to justify if the assumptions don't mention Unique

[Lukas Miaskiwskyi]

Does that have any precedent in mathlib, naming related statements consistently with respect to one another, but in contradiction with their direct assumptions? Otherwise I feel inclined to just leave things as they are, and hope that end-users will find their way through the docstrings linking the theorems. theorem prodUnique [Subsingleton S]looks dirty to me :)

[Yaël Dillies]

I mean, it's not even like the Unique in prodUnique really refers to an assumption.