Def FundamentalGroupoidFunctor.equivOfHomotopyEquiv

Modification history

2026-01-08 12:28

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

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

Modified FundamentalGroupoidFunctor.equivOfHomotopyEquiv View on Github →

2023-07-07 11:12

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

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

Added FundamentalGroupoidFunctor.equivOfHomotopyEquiv View on Github →