mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

feat(order/conditionally_complete_lattice): add `with_top.supr_coe_eq_top` and `with_top.supr_coe_lt_top`

Open j-loreaux opened this issue 3 years ago • 1 comments


golfing welcome if you feel the urge.

Open in Gitpod

j-loreaux avatar Aug 10 '22 14:08 j-loreaux

Thanks!

bors merge

ocfnash avatar Aug 15 '22 07:08 ocfnash

Build failed (retrying...):

bors[bot] avatar Aug 15 '22 09:08 bors[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 15 '22 12:08 bors[bot]