Def FundamentalGroupoidFunctor.homotopicMapsNatIso

Modification history

2023-07-07 11:12

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

feat: port AlgebraicTopology.FundamentalGroupoid.InducedMaps (#5756)

Added FundamentalGroupoidFunctor.homotopicMapsNatIso View on Github →