English
If each (η_i) is a type and (b_i) is a basis of M_i over R, then there is a natural basis on the direct sum DFinsupp fun i ↦ M_i, indexed by pairs (i, η_i), built from the b_i and the DFinsupp structure.
Русский
Пусть для каждого i задан базис b_i модуля M_i; тогда над модулем прямой суммы DFinsupp существует естественная база, индексируемая парами (i, η_i), построенная из базисов b_i и структуры DFinsupp.
LaTeX
$$$\\text{DFinsupp.basis }\\; (b_i) : \\text{Basis} (Σ i, η_i)\\; R\\; (Π_0 i, M_i)$$$
Lean4
/-- The basis on `ι →₀ M` with basis vectors `fun ⟨i, x⟩ ↦ single i (b i x)`. -/
protected def basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (Σ i, φ i) R (ι →₀ M) :=
.ofRepr <|
(finsuppLequivDFinsupp R).trans <|
(DFinsupp.mapRange.linearEquiv fun i ↦ (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm
