Commit 2024-06-12 23:50 f6f222ae

View on Github →

chore(Order/WithBot): add several simp, norm_cast lemmas (#13640)

Estimated changes

added theorem WithBot.coe_eq_top
added theorem WithBot.coe_top
added theorem WithBot.top_eq_coe
added theorem WithTop.bot_eq_coe
added theorem WithTop.coe_bot
added theorem WithTop.coe_eq_bot