distributivity of composition of continuous linear maps

Stream: mathlib4

[Sébastien Gouëzel]

I can't believe that we don't have distributivity of finset sums over composition of continuous linear maps, i.e.

import Mathlib
lemma foo {E F G 𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
    (A : ι → (E →L[𝕜] F)) (B : G →L[𝕜] E) : (∑ i, A i) ∘L B = ∑ i, ((A i) ∘L B) := sorry

Am I missing something?

[Notification Bot]

A message was moved here from #mathlib4 > Variables not imported by Sébastien Gouëzel.

[Sébastien Gouëzel]

@loogle ContinuousLinearMap, Finset.sum

[loogle]

:search: ContinuousLinearMap.map_sum, ContinuousLinearMap.coe_sum, and 69 more

[Sébastien Gouëzel]

@loogle Finset.sum, ContinuousLinearMap.comp

[loogle]

:shrug: nothing found

[Bhavik Mehta]

This looks like it should come from the fact that . ∘L B is a monoid hom, more specifically a monoid hom class. Do we have this instance?

[Yaël Dillies]

I don't see where the MonoidHomClass would be, but a MonoidHom I certainly believe!

[Sébastien Gouëzel]

It's not that the proof is hard (by ext; simp works fine). I was more surprised that nobody has needed this strongly enough to add it as a lemma in the library.

[Eric Wieser]

Do we have the ring structure on continuous endomorphisms?