Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-01-27 22:42
d074b51b
View on Github →
refactor(category_theory/concrete_category): move
bundled
to own file
Estimated changes
Modified
src/category_theory/category.lean
deleted
structure
category_theory.bundled
deleted
theorem
category_theory.bundled_hom_coe
deleted
structure
category_theory.concrete_category
deleted
theorem
category_theory.concrete_category_comp
deleted
theorem
category_theory.concrete_category_id
deleted
def
category_theory.mk_ob
Created
src/category_theory/concrete_category.lean
added
theorem
category_theory.bundled.bundled_hom_coe
added
theorem
category_theory.bundled.concrete_category_comp
added
theorem
category_theory.bundled.concrete_category_id
added
def
category_theory.bundled.map
added
structure
category_theory.bundled
added
structure
category_theory.concrete_category
added
def
category_theory.concrete_functor
added
def
category_theory.forget
added
def
category_theory.mk_ob
Modified
src/category_theory/examples/measurable_space.lean
Modified
src/category_theory/examples/monoids.lean
Modified
src/category_theory/examples/rings.lean
Modified
src/category_theory/examples/topological_spaces.lean
Modified
src/category_theory/functor.lean
deleted
def
category_theory.bundled.map
deleted
def
category_theory.concrete_functor
Modified
src/category_theory/types.lean
deleted
def
category_theory.forget