mathlib3

9adf9bb6 - feat(order/ideal): add partial_order instance to order.ideal (#5909)

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.