LinearEquiv version of LinearMap.pi

Stream: Is there code for X?

[Kenny Lau]

LinearMap.pi is (f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i

but I could not for the life of me find the LinearEquiv version of this map (or even Equiv)

[Kenny Lau]

in maths, I want $\operatorname{Hom}(M,N)^k \cong \operatorname{Hom}(M,N^k)$

[Kenny Lau]

It doesn't seem like it exists, since the product for ModuleCat is actually constructed with the unbundled version...

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/507dd92b9ed9cfd43bd29d1438a458da6705d8a0/Mathlib/Algebra/Category/ModuleCat/Products.lean#L29-L32

[Kenny Lau]

(after consulting the standard search engines, i've finally asked GPT as well, and it also couldn't find it)

[Eric Wieser]

I think @Junyan Xu has this in a PR

[Junyan Xu]

https://github.com/leanprover-community/mathlib4/pull/25284/files#diff-c46ac565cdc0776d5d57bb78877475b7c948445a4e99c179aa9aad88dfc4ea2aR108