Commit 2026-10-17 17:39 74e558e2

View on Github →

chore(Order/DirSupClosed): fix badly named theorems (#44974) I made a copy-paste error on the name of a deprecation in #44929. And back in #37670, I accidentally opened a namespace instead of a section... I haven't deprecated any of these badly named theorems. I want to believe that if anyone were using them downstream, they would have caught this already!

Estimated changes