Mathlib v3 is deprecated. Go to Mathlib v4

Theorem path.homotopic.hpath_hext

Modification history

2022-03-12 11:06
src/topology/homotopy/path.lean
feat(topology/homotopy): Homotopic maps induce naturally isomorphic functors between fundamental groupoid (#11595)
Added path.homotopic.hpath_hextView on Github →