Theorem WithBot.rec_bot_coe_coe

Modification history

2022-11-30 17:19

Mathlib/Order/WithBot.lean

chore: fix naming conventions in Order.WithBot (#801)

Deleted WithBot.rec_bot_coe_coe View on Github →

2022-11-29 20:56

Mathlib/Order/WithBot.lean

feat: port Order.WithBot (#777) …

Added WithBot.rec_bot_coe_coe View on Github →