finrank_zero_of_subsingleton — Mathlib

English

If n ≤ finrank R M, there exists a Finset s ⊆ M with s.card = n and LinearIndependent R ((↑) : s → M).

Русский

Если n ≤ finrank R M, существует Finset s ⊆ M с card n и LinearIndependent R (Subtype.val).

LaTeX

$$$\forall n:\, \mathbb{N},\; n \le \operatorname{finrank} R M \Rightarrow \exists s : \mathrm{Finset} M, s.card = n ∧ \operatorname{LinearIndependent} R ((\uparrow) : s \to M)$$$

Lean4

/-- A (finite-dimensional) space that is a subsingleton has zero `finrank`. -/
@[nontriviality]
theorem finrank_zero_of_subsingleton [Subsingleton M] : finrank R M = 0 := by rw [finrank, rank_subsingleton', map_zero]

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