mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Algebra/Category/*): simp lemmas for unbundled comp and categorical identities

Open kim-em opened this issue 1 year ago • 0 comments

These are useful in "mixed contexts" where we have categorical morphisms combined in "non-categorical" ways.

Open in Gitpod

kim-em avatar May 22 '24 06:05 kim-em