linearIndependent_iff_card_le_finrank_span

English

A finite family is linearly independent if and only if the cardinality equals the finrank of its span (simp edition).

Русский

Конечное семейство линейно независимо тогда и только тогда, когда число элементов равно финразмерности порожденного ими подпространства.

LaTeX

$$$\operatorname{linearIndependent}_K b \iff \operatorname{Fintype.card } ι = (\operatorname{Set.range} b).finrank_K$$$

Lean4

theorem linearIndependent_iff_card_le_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
    LinearIndependent K b ↔ Fintype.card ι ≤ (Set.range b).finrank K := by
  rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).ge_iff_eq']

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