mathlib

6285167a - chore(topology/algebra/module/basic): generalize `to_span_singleton` to topological spaces (#19116)

chore(topology/algebra/module/basic): generalize `to_span_singleton` to topological spaces (#19116) This should be straightforward to forward-port, as it involves deleting one hunk and pasting in another.