Theorem Submodule.isPathConnected

Modification history

2025-05-12 15:03
Mathlib/Analysis/Convex/PathConnected.lean
feat: define `Path.segment` (#24761) …
Modified Submodule.isPathConnectedView on Github →
2025-05-11 18:08
Mathlib/Analysis/Convex/Topology.lean
chore(Convex/Topology): golf (#24765) …
Added Submodule.isPathConnectedView on Github →