# 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.

Mathlib v3 is deprecated. Go to Mathlib v4

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.