Commit 2024-03-18 10:51 86b4c66b
View on Github →fix: rename LocallyFiniteOrderTop.ofIic to LocallyFiniteOrderBot (#11371)
It's about LocallyFiniteOrderBot, so the current name is simply wrong.
Also fix documentation mistakes. These errors were already present in Mathlib 3, before the port.