natCast_le_rank_iff_finset — Mathlib

English

For any n, n ≤ rank R M iff there exists a Finset s ⊆ M with card n and LinearIndependent R id on s.

Русский

Для любого n выполняется: n ≤ ранг R M эквивалентно существованию конечного подмножества s ⊆ M, такого что |s|=n и LinearIndepOn R id s.

LaTeX

$$$\forall n:\, \mathbb{N},\; n \le \operatorname{rank}_R(M) \iff \exists s : \mathrm{Finset} M, s.card = n ∧ \operatorname{LinearIndependent} R (\mathrm{id} : s \to M)$$$

Lean4

theorem natCast_le_rank_iff_finset [Nontrivial R] {n : ℕ} :
    n ≤ Module.rank R M ↔ ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) :=
  ⟨exists_finset_linearIndependent_of_le_rank, fun ⟨s, h₁, h₂⟩ ↦ by simpa [h₁] using h₂.cardinal_le_rank⟩

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