Naming of `inner_sum`/`sum_inner`

Stream: mathlib4

[Jovan Gerbscheid]

We have

inner_sum : inner x (∑ i ∈ s, f i) = ∑ i ∈ s, inner x (f i)
sum_inner : inner (∑ i ∈ s, f i) x = ∑ i ∈ s, inner (f i) x
inner_smul_right : inner x (r • y) = r * inner x y
inner_smul_left : inner (r • x) y = (starRingEnd 𝕜) r * inner x y

It seems to me like better names would be inner_sum_right and inner_sum_left. Or we should commit to using inner as an infix, giving smul_inner and inner_smul.