English
If rank_R M = n for some natural n, then finrank_R M = n (n ≥ 0).
Русский
Если ранг модуля M по R равен натуральному числу n, то finrank_R M = n.
LaTeX
$$$$\\\\operatorname{finrank}_R M = n \\\\text{ whenever } \\\\operatorname{rank}_R M = n.$$$$
Lean4
/-- The rank of a module as a natural number.
For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to
the dimension of `V` over `k`.
For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the
cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is
defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a
cardinal-valued version where infinite rank modules have rank an infinite cardinal.
Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but
`finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty
`ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons. -/
noncomputable def finrank (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] : ℕ :=
Cardinal.toNat (Module.rank R M)
