Theorems · Theorem · linear algebra

linearIndepOn_pair_iff

∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {i j : ι} (v : ι → V), i ≠ j → v i ≠ 0 → (LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j)

LinearIndepOn.pair_iff is a version that works over arbitrary rings.

Defined in

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModule