@[reducible, inline]

noncomputable abbrev Submodule.finrank {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : ℕ

The dimension of a submodule

Equations

• S.finrank = Module.finrank R ↥S