Commit 2023-11-08 21:29 21e2d926
View on Github →chore(Order): restore missing simp attribute (#8162)
This lemma was marked simp in mathlib3, and the attribute seems to have gone missing during the port.
chore(Order): restore missing simp attribute (#8162)
This lemma was marked simp in mathlib3, and the attribute seems to have gone missing during the port.