Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-05 03:14 0b7ee1b4

View on Github →

feat(category_theory): introduce the core of a category (#832)

Estimated changes

Created src/category_theory/core.lean

added theorem category_theory.core.comp_hom

added def category_theory.core.forget_functor_to_core

added def category_theory.core.functor_to_core

added theorem category_theory.core.id_hom

added def category_theory.core.inclusion

added def category_theory.core

Modified src/category_theory/isomorphism.lean

added theorem category_theory.functor.map_hom_inv

added theorem category_theory.functor.map_inv_hom