Theorem Path.Homotopic.pathCast

Modification history

2026-01-08 12:28

Mathlib/Topology/Homotopy/Path.lean

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

Added Path.Homotopic.pathCast View on Github →