exists_linearIndependent_snoc_of_lt_finrank

English

For a submodule N of a finite-rank module M, the standard rank-nullity formula gives finrank of the quotient plus finrank of N equals finrank of M.

Русский

Для подмодуля N модуля M с конечной размерностью верна формула ранга: finrank(M/N) + finrank(N) = finrank(M).

LaTeX

$$$\operatorname{finrank}_R(M/N) + \operatorname{finrank}_R(N) = \operatorname{finrank}_R(M).$$$

Lean4

/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v)
    (h : n < finrank R M) : ∃ (x : M), LinearIndependent R (Fin.snoc v x) :=
  exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h)

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