Theorem WithBot.unbot'_coe

Modification history

2025-02-13 07:36

Mathlib/Order/WithBot.lean

chore(WithBot): rename `unbot'` to `unbotD` (#21532)

Deleted WithBot.unbot'_coe View on Github →

2022-11-29 20:56

Mathlib/Order/WithBot.lean

feat: port Order.WithBot (#777) …

Added WithBot.unbot'_coe View on Github →