linearIndependent_single_of_ne_zero

English

If each v_i ≠ 0 in M_i, then the family i ↦ Pi.single i (v_i) is linearly independent.

Русский

Если каждый v_i ≠ 0 в M_i, то семейство i ↦ Pi.single i (v_i) линейно независимо.

LaTeX

$$LinearIndependent R (fun i => Pi.single i (v i))$$

Lean4

theorem linearIndependent_single_of_ne_zero {ι R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] [DecidableEq ι] {v : ι → M} (hv : ∀ i, v i ≠ 0) :
    LinearIndependent R fun i : ι ↦ Pi.single i (v i) :=
  by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact linearIndependent_single (fun i (_ : Unit) ↦ v i) <| by simp +contextual [Fintype.linearIndependent_iff, hv]

Похожие утверждения