mathlib

5775ef75 - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime (#6924)

feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime (#6924) - `ideal_inter_nonempty`: the intersection of any two ideals is nonempty. A preorder with joins and this property satisfies that its ideal poset is a lattice. - An ideal is prime iff `x \inf y \in I` implies `x \in I` or `y \in I`. - A maximal ideal in a distributive lattice is prime.