Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.concrete_category.has_coe_to_fun

Modification history

2021-10-21 02:55

src/category_theory/concrete_category/basic.lean

chore(*): bump to lean 3.34.0 (#9824) …

Modified category_theory.concrete_category.has_coe_to_fun View on Github →

2019-10-22 02:29

src/category_theory/concrete_category/basic.lean

refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491) …

Added category_theory.concrete_category.has_coe_to_fun View on Github →