mathlib

8e413ebb - feat(order/bounded_lattice): define atoms, coatoms, and simple lattices (#5471)

feat(order/bounded_lattice): define atoms, coatoms, and simple lattices (#5471) Defines `is_atom`, `is_coatom`, and `is_simple_lattice` Refactors `ideal.is_maximal` to use `is_coatom`, the new definition is definitionally equal to the old one Co-authored-by: Johan Commelin <johan@commelin.net>