Commit 2023-07-07 04:00 0726e5e6

View on Github →

feat: port AlgebraicTopology.FundamentalGroupoid.Product (#5696)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

added def FundamentalGroupoidFunctor.coneDiscreteComp

added theorem FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone

added def FundamentalGroupoidFunctor.piIso

added def FundamentalGroupoidFunctor.piToPiTop

added def FundamentalGroupoidFunctor.piTopToPiCone

added def FundamentalGroupoidFunctor.preservesProduct

added def FundamentalGroupoidFunctor.prodIso

added def FundamentalGroupoidFunctor.prodToProdTop

added theorem FundamentalGroupoidFunctor.prodToProdTop_map

added def FundamentalGroupoidFunctor.proj

added def FundamentalGroupoidFunctor.projLeft

added theorem FundamentalGroupoidFunctor.projLeft_map

added def FundamentalGroupoidFunctor.projRight

added theorem FundamentalGroupoidFunctor.projRight_map

added theorem FundamentalGroupoidFunctor.proj_map