Theorem Submodule.closure_coe_iSup_map_single

Modification history

2025-03-12 03:44
Mathlib/Topology/Algebra/Module/Basic.lean
feat(Topology/): add `Submodule.closure_coe_iSup_map_single` (#22752) …
Added Submodule.closure_coe_iSup_map_singleView on Github →