Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.prod.category.inr

Modification history

2018-08-11 03:59
category_theory/products.lean
fix(category_theory): consistent use of coercions, consistent naming (#248)
Deleted category_theory.prod.category.inrView on Github →
2018-08-08 00:44
category_theory/products.lean
refactor(category_theory/products): tweak PR after merge
Added category_theory.prod.category.inrView on Github →