English
The dimension of a module M over a ring R is zero if and only if every element of M is zero in the sense of rank; more precisely, rank R M = 0 iff all elements vanish under a certain linear dependence criterion.
Русский
Размерность модуля M равна нулю тогда и только тогда, когда каждый элемент M равен нулю в определении ранга (символически говоря).
LaTeX
$$$\operatorname{rank}_R M = 0 \iff \forall x \in M,\; \exists a \in R,\; a \neq 0 \land a \cdot x = 0.$$$
Lean4
/-- If every finite set of linearly independent vectors has cardinality at most `n`,
then the same is true for arbitrary sets of linearly independent vectors.
-/
theorem linearIndependent_bounded_of_finset_linearIndependent_bounded {n : ℕ}
(H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
∀ s : Set M, LinearIndependent R ((↑) : s → M) → #s ≤ n :=
by
intro s li
apply Cardinal.card_le_of
intro t
rw [← Finset.card_map (Embedding.subtype s)]
apply H
apply linearIndependent_finset_map_embedding_subtype _ li
