Direct sum on fintype

Stream: Is there code for X?

[Heather Macbeth]

We have constructions docs#finsupp.equiv_fun_on_fintype, docs#finsupp.linear_equiv_fun_on_fintype, etc, giving an equivalence, for [fintype ι], of ι → F with its finitely-supported subtype.

I couldn't find the equivalence for the more general situation of a varying family Π i, E i. Is it indeed missing?

import algebra.direct_sum.module

noncomputable theory

variables {ι : Type*} [fintype ι] {R : Type*} [ring R]
variables {F : Type*} [add_comm_group F] [module R F]
variables {E : ι → Type*} [Π i, add_comm_group (E i)] [Π i, module R (E i)]

open_locale direct_sum

example : (ι →₀ F) ≃ₗ[R] (ι → F) := finsupp.linear_equiv_fun_on_fintype R F ι

example : (⨁ i, E i) ≃ₗ[R] Π i, E i := sorry

[Yury G. Kudryashov]

git grep fintype in algebra/direct_sum gives no results.

[Yury G. Kudryashov]

So, you'll have to define it yourself.

[Eric Wieser]

It should probably be defined for dfinsupp too / instead

[Heather Macbeth]

#9664