exists_linearIndependent_pair_of_one_lt_finrank

English

If the rank is greater than 1, then for every nonzero x ∈ M there exists y with {x,y} LI.

Русский

Если ранк больше единицы, для каждого ненулевого x существует y такой, что {x,y} линейно независимо.

LaTeX

$$$\forall x \in M, x \neq 0 \Rightarrow \exists y \in M: \{x,y\} \text{ is LI}. $$$

Lean4

/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another
vector linearly independent of the first one. -/
theorem exists_linearIndependent_pair_of_one_lt_finrank [NoZeroSMulDivisors R M] (h : 1 < finrank R M) {x : M}
    (hx : x ≠ 0) : ∃ y, LinearIndependent R ![x, y] :=
  exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx

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