English
Let M be an R-module of rank greater than 1 and let x ∈ M with x ≠ 0. Then there exists y ∈ M such that {x, y} is a linearly independent set over R.
Русский
Пусть M – модуль над кольцом R, допускающий размерность более 1, и пусть x ∈ M непроизвольный. Тогда существует y ∈ M такое, что {x, y} линейно независимо над R.
LaTeX
$$$\text{Let } M \text{ be an } R\text{-module with } \operatorname{rank}_R M > 1. \text{ If } x \in M, x \neq 0, \text{ then there exists } y \in M \text{ such that } \{x, y\} \text{ is linearly independent}. $$$
Lean4
/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly
independent of the first one. -/
theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R] [NoZeroSMulDivisors R M]
(h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) : ∃ y, LinearIndependent R ![x, y] :=
by
obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h
have : Fin.snoc ![x] y = ![x, y] := by simp [Fin.snoc, ← List.ofFn_inj]
rw [this] at hy
exact ⟨y, hy⟩
