English
The rank of a module is defined as the supremum of the sizes of linearly independent subsets; for rings with the strong rank condition this coincides with the dimension (the cardinality of a basis) for free modules and agrees with the usual notion of dimension for vector spaces.
Русский
Ранг модуля определяется как наибольшая по кардиналу размер линейно независимых подмножеств; для колец с условием сильного ранга этот ранг совпадает с размерностью свободного модуля (мощность базиса) и согласуется с обычной размерностью векторного пространства.
LaTeX
$$$\operatorname{rank}_R(M) = \sup\{ |S| : S \subseteq M, \; S \text{ линейно независимо над } R \}$$$
Lean4
/-- The rank of a module, defined as a term of type `Cardinal`.
We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.
For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).
In particular this agrees with the usual notion of the dimension of a vector space.
See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).
-/
def rank :=
val_proj @wrapped✝.{}
