English
The linear independence of the map ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) follows from the corresponding injectivity/isomorphism between finsupp representations and DFinsupp representations, via a transfer of linear independence from (f i).
Русский
Линейная независимость отображения ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) следует из переноса линейной независимости между представлениями Finsupp и DFinsupp через соответствующий биективный переход от (f_i).
LaTeX
$$$\\text{LinearIndependent } R\\bigl(\\lambda ix. \\mathrm{single}_{ix.1}(f_{ix.1}(ix.2))\\bigr)$$$
Lean4
theorem linearIndependent_single {φ : ι → Type*} (f : ∀ i, φ i → M) (hf : ∀ i, LinearIndependent R (f i)) :
LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) := by
classical
convert (DFinsupp.linearIndependent_single _ hf).map_injOn _ (finsuppLequivDFinsupp R).symm.injective.injOn
simp
