linearIndependent_single_of_ne_zero

English

If R is a ring with NoZeroSmulDivisors in M and each v_i ≠ 0, then the family i ↦ single i (v_i) is linearly independent.

Русский

Если имеется кольцо R с свойством NoZeroSmulDivisors и все v_i ≠ 0, то семейство i ↦ single i (v_i) линейно независимо.

LaTeX

$$$\\text{LinearIndependent } R\\; (\\lambda i. \\mathrm{single}_i(v_i))$ under NoZeroSmulDivisors$$

Lean4

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

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