Naming of `finprod_mem` lemmas

Stream: mathlib4

[Christian Merten]

On PR #23849, @Yaël Dillies is suggesting to name lemmas like docs#finprod_mem_def, bfinprod_def instead. i.e. replace finprod_mem by bfinprod mirroring names like docs#Set.mem_biUnion.

I think finprod_mem is perfectly following the symbol reading convention and is followed consistently (Loogle shows 0 usages of bfinprod), so I see no reason why to switch to bfinprod instead.

What do people think?

[Eric Wieser]

I think this issue is the clash with docs#prod_mem

[Aaron Liu]

Why is that not namespaced?

[Riccardo Brasca]

Aaron Liu said:

Why is that not namespaced?

Surely a mistake.

[Eric Wieser]

To match docs#multiset_prod_mem

[Eric Wieser]

I think probably that should be multisetProd_mem

[Aaron Liu]

I was thinking Multiset.prod_mem

[Aaron Liu]

certainly I wouldn't be searching for multisetProd_mem

[Aaron Liu]

Maybe that should be protected

[Eric Wieser]

see also docs#dfinsuppProd_mem

[Aaron Liu]

I see it, and I'm thinking it should be DFinsupp.prod_mem

[Eric Wieser]

I'd argue the naming convention permits both

[Aaron Liu]

I guess

[Eric Wieser]

Probably the naming originates from when we had separate Submonoid.dfinsuppProd_mem etc lemmas

[Aaron Liu]

I see, that makes sense