exists_linearIndependent_of_le_finrank

English

If n ≤ finrank R M, there exists f: Fin n → M that is LinearIndependent.

Русский

Если n ≤ finrank_R(M), существует f: Fin n → M линейно независимое.

LaTeX

$$$\forall n\, (hn : n ≤ \operatorname{finrank}_R(M))\; \exists f : \mathrm{Fin}\,n \to M, \operatorname{LinearIndependent} R f$$$

Lean4

theorem exists_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) :
    ∃ f : Fin n → M, LinearIndependent R f :=
  have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_finrank hn
  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩

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