mathlib
5bf57407 - chore(category_theory/fin_category): Speed up `as_type_equiv_obj_as_type` (#13298)

Commit
3 years ago
chore(category_theory/fin_category): Speed up `as_type_equiv_obj_as_type` (#13298) Rename `obj_as_type_equiv_as_type` to `as_type_equiv_obj_as_type` (likely a typo). Use `equivalence.mk` instead of `equivalence.mk'` to build it and split the functors to separate definitions to tag them with `@[simps]` and make `dsimp` go further. On my machine, this cuts down the compile time from 41s to 3s.
Author
Parents
Loading