linearIndepOn_pair_iff — Mathlib

English

Over an arbitrary ring, for i ≠ j and v i ≠ 0, LinearIndepOn K v {i,j} is equivalent to the condition that for all c ∈ K, c v i ≠ v j.

Русский

Для i ≠ j и v i ≠ 0, линейная независимость на {i,j} эквивалентна тому, что для всех c ∈ K, c v i ≠ v j.

LaTeX

$$$\text{LinearIndepOn}_K v\{i,j\} \iff \forall c \in K,\ c \cdot v i \neq v j$$$

Lean4

/-- `LinearIndepOn.pair_iff` is a version that works over arbitrary rings. -/
theorem linearIndepOn_pair_iff {i j : ι} (v : ι → V) (hij : i ≠ j) (hi : v i ≠ 0) :
    LinearIndepOn K v { i, j } ↔ ∀ (c : K), c • v i ≠ v j :=
  by
  rw [pair_comm]
  convert linearIndepOn_insert (s := { i }) (a := j) hij.symm
  simp [hi, mem_span_singleton]

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