finset.sum_smul

Stream: mathlib4

[Xavier Roblot]

In mathlib4#1665, the mathlib3 lemma finset.sum_smul is automatically translated to Finset.sum_smul which is correct. The statement is:

theorem Finset.sum_smul {f : ι → R} {s : Finset ι} {x : M} :
    (∑ i in s, f i) • x = ∑ i in s, f i • x

But that causes a name clash since there is already a docs4#Finset.sum_smul declared in Mathlib.Algebra.BigOperators.Basic and created by to_additive. But this one should be called Finset.sum_nsmul instead to align with the mathlib3 name.

So the way to fix that is to create another PR to fix names in Mathlib.Algebra.BigOperators.Basic, I guess?

[Ruben Van de Velde]

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20translating.20pow.20to.20nsmul

[Xavier Roblot]

mathlib4#1671