Commit 2022-03-12 02:28 09d0f028

View on Github →

chore({category_theory,order}/category/*): Missing dsimp lemmas (#12593) Add the dsimp lemmas stating ↥(of α) = α . Also rename the few to_dual functors to dual to match the other files.

Estimated changes