mathlib
dddf6ebe - feat(data/fintype/order): More and better instances (#11702)

Commit
3 years ago
feat(data/fintype/order): More and better instances (#11702) In a fintype, this allows to promote * `distrib_lattice` to `complete_distrib_lattice` * `boolean_algebra` to `complete_boolean_algebra` Also strengthen * `fintype.to_order_bot` * `fintype.to_order_top` * `fintype.to_bounded_order` * `complete_linear_order.to_conditionally_complete_linear_order_bot`
Author
Parents
Loading