Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-21 18:29 6285167a

View on Github →

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.

Estimated changes