Def WithBot.insertBot

Modification history

2025-03-05 05:17
Mathlib/Order/Interval/Finset/Defs.lean
feat: WithBot.insertBot (#22523) …
Added WithBot.insertBotView on Github →