LinearMap.piCongrRight

Stream: Is there code for X?

[Eric Wieser]

Do we have this?

import Mathlib

variable {ι R} {M N : ι → Type*} [Semiring R]
  [∀ i, AddCommMonoid (M i)][∀ i, Module R (M i)]
  [∀ i, AddCommMonoid (N i)][∀ i, Module R (N i)]

/-- `Pi.map` as a linear map. -/
def LinearMap.piCongrRight (f : ∀ i, M i →ₗ[R] N i) :
    (Π i, M i) →ₗ[R] (Π i, N i) where
  toFun := Pi.map (f ·)
  map_add' _ _ := funext fun _ => map_add _ _ _
  map_smul' _ _ := funext fun _ => map_smul _ _ _

[Eric Wieser]

Phrased another way, this is the n-ary version of docs#LinearMap.prodMap

[Eric Wieser]

Or the right version of docs#LinearMap.funLeft

[Dexin Zhang]

Is docs#LinearMap.compLeft its non-dependent version?

[Weiyi Wang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectSum/Module.html#DirectSum.lmap is this close? sorry, not right

[Eric Wieser]

Nice find, thanks @Dexin Zhang!

[Eric Wieser]

That doesn't work for me, but at least tells me what to clean up if I PR the above