noncomputable def Submodule.finrank {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Submodule R M) : ℕ

Equations

• s.finrank = Module.finrank R ↥s