Theorem CategoryTheory.Functor.precomp_map_hEq

Modification history

2023-07-07 11:12

Mathlib/CategoryTheory/EqToHom.lean

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

Deleted CategoryTheory.Functor.precomp_map_hEq View on Github →

2023-02-11 14:45

Mathlib/CategoryTheory/EqToHom.lean

feat port/CategoryTheory.EqToHom (#2207)

Added CategoryTheory.Functor.precomp_map_hEq View on Github →