Commit 2023-02-22 03:15 f89a71d4

View on Github →

feat: port/CategoryTheory.Category.Cat (#2375)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Cat.lean

added theorem CategoryTheory.Cat.comp_map

added theorem CategoryTheory.Cat.comp_obj

added def CategoryTheory.Cat.equivOfIso

added theorem CategoryTheory.Cat.id_map

added def CategoryTheory.Cat.objects

added def CategoryTheory.Cat.of

added def CategoryTheory.Cat

added def CategoryTheory.typeToCat