Commit 2021-01-27 12:14 9adf9bb6

feat(order/ideal): add partial_order instance to order.ideal (#5909) Add some instances for order.ideal, some of them conditional on having extra structure on the carrier preorder P:

• In all cases, ideal P is a partial order.
• If P has a bottom element, so does ideal P.
• If P has a top element, so does ideal P. (Although this could be weekened to P being directed.) Also, add some @[ext], @[simp], @[trans] lemmas.