Commit 2024-04-24 19:18 cba2f37b

View on Github →

feat(CategoryTheory/EqToHom): generalize Functor.congr_map to Prefunctor.congr_map (#12384)

Estimated changes

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

deleted theorem CategoryTheory.Functor.congr_map

Modified Mathlib/Combinatorics/Quiver/Basic.lean

added theorem Prefunctor.congr_map