Theorem Submodule.smul_top_eq_range_lsum

Modification history

2026-02-26 23:39
Mathlib/LinearAlgebra/Finsupp/Span.lean
feat(LinearAlgebra/Finsupp): add lemmas about `lsum` and submodule (#35660) …
Added Submodule.smul_top_eq_range_lsumView on Github →