linearIndependent_single_ne_zero — Mathlib

English

For a family v with each v_i ≠ 0, the Pi.single i (v_i) are linearly independent.

Русский

Для семейства v с каждым v_i ≠ 0, элементы Pi.single i (v_i) линейно независимы.

LaTeX

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

Lean4

@[deprecated linearIndependent_single_of_ne_zero (since := "2025-04-14")]
theorem linearIndependent_single_ne_zero {ι R : Type*} [Ring R] [NoZeroDivisors R] [DecidableEq ι] {v : ι → R}
    (hv : ∀ i, v i ≠ 0) : LinearIndependent R (fun i : ι ↦ Pi.single i (v i)) :=
  linearIndependent_single_of_ne_zero hv

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