Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-12-20 23:12
73933b73
View on Github →
feat(category_theory): assorted small changes from the old limits PR (
#512
)
Estimated changes
Modified
algebra/pi_instances.lean
added
def
pi.is_ring_hom_pi
Modified
category_theory/category.lean
added
theorem
category_theory.bundled_hom_coe
added
theorem
category_theory.category.assoc_symm
Created
category_theory/discrete_category.lean
added
theorem
category_theory.discrete.functor_map_id
added
def
category_theory.discrete.lift
added
def
category_theory.discrete
added
def
category_theory.functor.of_function
added
def
category_theory.nat_trans.of_function
Modified
category_theory/examples/rings.lean
modified
def
category_theory.examples.CommRing.forget_to_CommMon
added
theorem
category_theory.examples.CommRing_hom_coe_app
deleted
def
category_theory.examples.is_comm_ring_hom
Modified
category_theory/examples/topological_spaces.lean
deleted
def
category_theory.examples.map
deleted
def
category_theory.examples.map_id
deleted
theorem
category_theory.examples.map_id_obj
deleted
def
category_theory.examples.map_iso
deleted
def
category_theory.examples.map_iso_id
added
def
topological_space.opens.map
added
def
topological_space.opens.map_id
added
theorem
topological_space.opens.map_id_obj
added
def
topological_space.opens.map_iso
added
def
topological_space.opens.map_iso_id
Modified
category_theory/functor.lean
Modified
category_theory/functor_category.lean
Modified
category_theory/limits/cones.lean
Modified
category_theory/limits/limits.lean
added
theorem
category_theory.limits.colimit.desc_extend
added
theorem
category_theory.limits.limit.lift_extend
Modified
category_theory/opposites.lean
Modified
category_theory/pempty.lean
modified
def
category_theory.functor.empty
Modified
category_theory/punit.lean
deleted
theorem
category_theory.functor.of.map_app
deleted
theorem
category_theory.functor.of.obj_map
deleted
theorem
category_theory.functor.of.obj_obj
deleted
def
category_theory.functor.of
Created
data/ulift.lean
added
theorem
plift.rec.constant
added
theorem
ulift.rec.constant
Modified
tactic/ext.lean
added
theorem
plift.ext