Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.discrete.comp_nat_iso_discrete

Modification history

2022-03-05 15:19
src/category_theory/discrete_category.lean
feat(category_theory/discrete_category): generalize universes for comp_nat_iso_discrete (#12340)
Modified category_theory.discrete.comp_nat_iso_discreteView on Github →
2022-02-02 07:21
src/category_theory/discrete_category.lean
feat(topology/homotopy): Fundamental groupoid preserves products (#11459)
Added category_theory.discrete.comp_nat_iso_discreteView on Github →