Theorem WithBot.le_coe_unbot'

Modification history

2025-02-13 07:36

Mathlib/Order/WithBot.lean

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

Deleted WithBot.le_coe_unbot'View on Github →

2025-02-12 11:53

Mathlib/Order/WithBot.lean

chore(Order/WithBot): golf, clean up (#21274) …

Modified WithBot.le_coe_unbot'View on Github →

2024-01-23 09:49

Mathlib/Order/WithBot.lean

feat(Order/WithBot): add `WithBot.lt_coe_bot` (#9898) …

Modified WithBot.le_coe_unbot'View on Github →

2022-11-29 20:56

Mathlib/Order/WithBot.lean

feat: port Order.WithBot (#777) …

Added WithBot.le_coe_unbot'View on Github →