finrank_eq_zero_of_infinite — Mathlib

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) \Rightarrow \exists f : \mathrm{Fin}\,n \to M, \operatorname{LinearIndependent} R f$$$

Lean4

theorem finrank_eq_zero_of_infinite {ι} [Infinite ι] {v : ι → M} (hv : LinearIndependent R v) : finrank R M = 0 :=
  toNat_eq_zero.mpr <| .inr hv.aleph0_le_rank

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