Theorem Submodule.connectedComponentIn_eq_self_of_one_lt_codim

Modification history

2024-04-17 13:43
Mathlib/Analysis/NormedSpace/Connected.lean
feat: codimension two subspaces have path-connected complement (#11337) …
Added Submodule.connectedComponentIn_eq_self_of_one_lt_codimView on Github →