English
Given a family of independent vectors v_i in modules M_i, the family of functions ji ↦ Pi.single ji.1 (v ji.1 ji.2) is linearly independent.
Русский
Пусть v_i — линейно независимые в соответствующих модулях, тогда семейство функций ji ↦ Pi.single ji.1 (v ji.1 ji.2) линейно независимо.
LaTeX
$$LinearIndependent R (fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2))$$
Lean4
theorem linearIndependent_single [Semiring R] [∀ i, AddCommMonoid (Ms i)] [∀ i, Module R (Ms i)] [DecidableEq η]
(v : ∀ j, ιs j → Ms j) (hs : ∀ i, LinearIndependent R (v i)) :
LinearIndependent R fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2) := by
convert (DFinsupp.linearIndependent_single _ hs).map_injOn _ DFinsupp.injective_pi_lapply.injOn
