feat(linear_algebra/finsupp): add mem_span_set (#6457)
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





leanprover-community/mathlib,leanprover-community/mathlib