Commit 2026-02-26 23:39 fe8cb25d
View on Github →feat(LinearAlgebra/Finsupp): add lemmas about lsum and submodule (#35660)
This is split from #34936 to make the review process easier.
It adds some lemmas to characterize the span of finitely supported singletons and relate the range of Finsupp.lsum to the pointwise scalar multiplication of submodules.