natCast_le_rank_iff — Mathlib

English

Assuming R is nontrivial, for any n ∈ N, n ≤ rank R M iff there exists a LI f: Fin n → M.

Русский

Пусть R не тривиально, тогда для любого n ∈ N выполняется: n ≤ ранг R M эквивалентно существованию LI-функции f: Fin n → M.

LaTeX

$$$[\text{Nontrivial } R] \;\Rightarrow\; (n \le \operatorname{rank}_R(M) \iff \exists f : \mathrm{Fin}\,n \to M, \operatorname{LinearIndependent} R f)$$$

Lean4

theorem natCast_le_rank_iff [Nontrivial R] {n : ℕ} : n ≤ Module.rank R M ↔ ∃ f : Fin n → M, LinearIndependent R f :=
  ⟨exists_linearIndependent_of_le_rank, fun H ↦ by simpa using H.choose_spec.cardinal_lift_le_rank⟩

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