Naming inconstency, finsum and multiplication

Stream: mathlib4

[Stefan Kebekus]

I would like to ask for advice on fixing a very minor naming inconsistency. Looking at Mathlib.Algebra.BigOperators.Finprod, I see theorems

• smul_finsum, which asks for the non-existence of zero divisors
• smul_finsum', which asks for finiteness of support
• mul_finsum, which asks for finiteness of support

A theorem mul_finsum', which asks for the non-existence of zero divisors, does not exist.

Should we rename one of the theorems for uniform naming? If so, which one? Or should we rename all of them, exposing the assumptions in the theorem names?

[Anne Baanen]

(I think you missed a prime in the second smul_finsum.)

[Anne Baanen]

If we do the renaming, we should not forget the finsum_smul etc versions too.

[Anne Baanen]

As far as I can tell, none of these lemmas is ever used in Mathlib? So it is hard to say which one is the most useful right now. It does seem common however scrolling through the file that the primed version of a lemma is more general and asks for a specific Support to be finite. So consistency suggests to use mul_finsum' for the finite Support version. (Note: I have not really used finsum/finprod in any large capacity.)

[Stefan Kebekus]

Anne Baanen schrieb:

(I think you missed a prime in the second smul_finsum.)

Oops. Thanks, I fixed that.

[Stefan Kebekus]

Thanks for the help. PR #30326 establishes commutativity between multiplication and finsum for rings without zero divisors and fixes the naming following @Anne Baanen's suggestion. And, of course, I asked Vierkantor to review…