feat(linear_algebra/finsupp): add mem_span_set (#6457)
From the doc-string:
If `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, then we can write
`m` as a finite `R`-linear combination of elements of `s`.
The implementation uses `finsupp.sum`.
The initial proof was a substantial simplification of mine, due to Kevin Buzzard. The final one is due to Eric Wieser.
Zulip discussion for the proof:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/submodule.2Espan.20as_sum
Zulip discussion for the universe issue:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universe.20issue.20with.20.60Type*.60
