the linear equivalence (ι →₀ M) ≃ₗ[A] ⨁ (i : ι), M

Stream: Is there code for X?

[Joël Riou]

import Mathlib.Algebra.DirectSum.Module
import Mathlib.Data.Finsupp.ToDFinsupp

open DirectSum

def finsuppLinearEquivDFinsupp (A M ι : Type*) [Ring A] [AddCommGroup M] [Module A M]
    [DecidableEq ι] [∀ (m : M), Decidable (m ≠ 0)]:
    (ι →₀ M) ≃ₗ[A] ⨁ (i : ι), M := by
  sorry

We have the additive equivalence finsuppAddEquivDFinsupp, but I do not find the linear equivalence version!?

[Eric Wieser]

docs#finsuppLequivDFinsupp

[Eric Wieser]

Probably it should be renamed

[Joël Riou]

Thanks very much!