Theorem Submodule.length_le_length_restrictScalars

Modification history

2026-04-15 00:18
Mathlib/RingTheory/Length.lean
feat(RingTheory): adds two lemmas on `Module.length` (#36657) …
Added Submodule.length_le_length_restrictScalarsView on Github →