mathlib3

b449a3cd - feat(order/ideal, order/pfilter, order/prime_ideal): added `is_ideal`, `is_pfilter`, `is_prime`, `is_maximal`, `prime_pair` (#6656)

feat(order/ideal, order/pfilter, order/prime_ideal): added `is_ideal`, `is_pfilter`, `is_prime`, `is_maximal`, `prime_pair` (#6656) Proved basic lemmas about them. Also extended the is_proper API. Made the `pfilter`arguments of some lemmas explicit: - `pfilter.nonempty` - `pfilter.directed`