Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-11 03:59 6bf879d2

View on Github →

fix(category_theory): consistent use of coercions, consistent naming (#248)

Estimated changes

Modified category_theory/functor.lean

modified theorem category_theory.functor.comp_obj

Modified category_theory/products.lean

deleted theorem category_theory.prod.category.comp

deleted def category_theory.prod.category.fst

deleted theorem category_theory.prod.category.id

deleted def category_theory.prod.category.inl

deleted def category_theory.prod.category.inr

deleted def category_theory.prod.category.snd

added def category_theory.prod.fst

added def category_theory.prod.inl

added def category_theory.prod.inr

added def category_theory.prod.snd

added theorem category_theory.prod_comp

added theorem category_theory.prod_id