Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-05 05:02 4af39760

View on Github →

chore(category_theory): cleanup (#1173)

chore(category_theory): cleanup
oops
remove comment
more uniform?
fix stalks proof?
Update src/algebra/CommRing/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
Apply suggestions from code review Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

Modified src/algebra/CommRing/basic.lean

deleted theorem CommRing.comp_val

deleted theorem CommRing.id_val

modified def CommRing.is_comm_ring_hom

Modified src/algebra/CommRing/colimits.lean

modified theorem CommRing.colimits.cocone_naturality_components

Modified src/algebra/Mon/colimits.lean

modified theorem Mon.colimits.cocone_naturality_components

Modified src/category_theory/concrete_category.lean

added theorem category_theory.bundled.coe_comp

Modified src/category_theory/isomorphism.lean

added theorem category_theory.functor.map_inv

Modified src/category_theory/limits/opposites.lean

Modified src/category_theory/opposites.lean

added def category_theory.is_iso_of_op

Modified src/category_theory/whiskering.lean

Modified src/topology/Top/stalks.lean

Modified src/topology/algebra/TopCommRing/basic.lean

modified def TopCommRing.forget