# Results on direct sums and finitely supported functions. #

1. The linear equivalence between finitely supported functions `ι →₀ M` and the direct sum of copies of `M` indexed by `ι`.

source
def finsuppLEquivDirectSum (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] :
(ι →₀ M) ≃ₗ[R] DirectSum ι fun (x : ι) => M

The finitely supported functions `ι →₀ M` are in linear equivalence with the direct sum of copies of M indexed by ι.

Equations

- finsuppLEquivDirectSum R M ι = finsuppLequivDFinsupp R

Instances For

source
@[simp]
theorem finsuppLEquivDirectSum_single (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] (i : ι) (m : M) :
(finsuppLEquivDirectSum R M ι) (Finsupp.single i m) = (DirectSum.lof R ι (fun (i : ι) => M) i) m
source
@[simp]
theorem finsuppLEquivDirectSum_symm_lof (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] (i : ι) (m : M) :
(finsuppLEquivDirectSum R M ι).symm ((DirectSum.lof R ι (fun (x : ι) => M) i) m) = Finsupp.single i m