theorem Submodule.finrank_congr {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (h : p = q) : Module.finrank R ↥p = Module.finrank R ↥q

theorem Submodule.finrank_lt_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Submodule K V} : Module.finrank K ↥s < Module.finrank K V ↔ s < ⊤