mathlib

ce31c1c6 - feat(order/prime_ideal): prime ideals are maximal (#9004)

feat(order/prime_ideal): prime ideals are maximal (#9004) Proved that in boolean algebras: 1. An ideal is prime iff it always contains one of x, x^c 2. A prime ideal is maximal