Commit 2025-04-17 13:52 1f4ab9d5
View on Github →feat: add lemma Submodule.length_lt (#24133)
This lemma is useful for reasoning inductively based on module length (in combination with a natural-number-valued length function for finite-length modules).