Commit 2026-04-15 00:18 11873348

feat(RingTheory): adds two lemmas on Module.length (#36657) This PR adds two lemmas regarding the length of modules:

• Submodule.length_le_restrictScalar shows that the length of an $R$-submodule is less than or equal to its length as an $A$-submodule under scalar restriction.
• Submodule.length_quotient_lt shows that for a module of finite length, the length of a quotient module $M \big/ p$ is strictly less than the length of $M$ when the submodule $p$ is non-trivial.