Def IsBotOneClass.toOrderBot

Modification history

2026-05-06 19:54
Mathlib/Algebra/Order/IsBotOne.lean
feat: `IsBotOneClass` and `IsBotZeroClass` (#38730) …
Added IsBotOneClass.toOrderBotView on Github →