Theorem Submodule.closure_subset_topologicalClosure_span

Modification history

2023-09-14 09:08
Mathlib/Topology/Algebra/Module/Basic.lean
feat: the linear span of a separable set is separable (#7115)
Added Submodule.closure_subset_topologicalClosure_spanView on Github →