mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat(LightCondensed): the functor from `TopCat`

Open dagurtomas opened this issue 1 year ago • 1 comments

  • [ ] depends on: #10412

Open in Gitpod

dagurtomas avatar Mar 27 '24 14:03 dagurtomas

This PR/issue depends on:

leanprover-community-mathlib4-bot avatar Mar 27 '24 14:03 leanprover-community-mathlib4-bot

This is independent of the refactor of LightProfinite. See #13504

dagurtomas avatar Jun 04 '24 13:06 dagurtomas