Def Path.Homotopy.pathCast

Modification history

2026-01-08 12:28

Mathlib/Topology/Homotopy/Path.lean

feat(FundamentalGroupoid/InducedMaps): generalize to different universes (#33445) …

Added Path.Homotopy.pathCast View on Github →