exists_linearIndependent_snoc_of_lt_rank

English

If hv: LinearIndependent R v and rank_R M > n, there exists x ∈ M such that Fin.snoc v x is linear independent.

Русский

Если hv: LinearIndependent R v и rank_R M > n, существует x ∈ M, такое что Fin.snoc v x линейно независимо.

LaTeX

$$$\exists x\, ( \operatorname{LinearIndependent} R (\operatorname{Fin.snoc} v\, x) )$$$

Lean4

/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_snoc_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < Module.rank R M) : ∃ (x : M), LinearIndependent R (Fin.snoc v x) :=
  by
  simp only [Fin.snoc_eq_cons_rotate]
  have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h
  exact ⟨x, hx.comp _ (finRotate _).injective⟩

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