English
If each module M i is free over R, then the direct sum DFinsupp fun i ↦ M i is also a free R-module. A basis for this direct sum is constructed from the bases of the individual M i.
Русский
Если каждый модуль M_i свободен над кольцом R, то и прямую сумму DFinsupp fun i ↦ M_i можно рассматривать как свободный модуль над R. База для этой суммы строится из баз каждого M_i.
LaTeX
$$$\\text{Module.Free } R\\left(\\Pi_{0} i, M_i\\right)$$$
Lean4
/-- The direct sum of free modules is free.
Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) : Basis (Σ i, η i) R (Π₀ i, M i) :=
.ofRepr ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)
