# mathlibdocumentation

algebra.direct_sum.finsupp

# 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 ι.
noncomputable def finsupp_lequiv_direct_sum (R : Type u) (M : Type v) [ring R] [ M] (ι : Type u_1) [decidable_eq ι] :
→₀ M) ≃ₗ[R] (λ (i : ι), M)

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

Equations
@[simp]
theorem finsupp_lequiv_direct_sum_single (R : Type u) (M : Type v) [ring R] [ M] (ι : Type u_1) [decidable_eq ι] (i : ι) (m : M) :
ι) m) = ι (λ (i : ι), M) i) m
@[simp]
theorem finsupp_lequiv_direct_sum_symm_lof (R : Type u) (M : Type v) [ring R] [ M] (ι : Type u_1) [decidable_eq ι] (i : ι) (m : M) :
ι).symm) ( ι (λ (i : ι), M) i) m) =