Commit 2020-12-29 07:47 8e413ebb

View on Github →

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

Estimated changes

Created src/order/atoms.lean

added theorem eq_bot_or_eq_of_le_atom

added theorem eq_top_or_eq_of_coatom_le

added def is_atom

added theorem is_atom_iff_is_coatom_dual

added theorem is_atom_top

added def is_coatom

added theorem is_coatom_bot

added theorem is_coatom_iff_is_atom_dual

added theorem is_simple_lattice_iff_is_atom_top

added theorem is_simple_lattice_iff_is_coatom_bot

added theorem is_simple_lattice_iff_is_simple_lattice_order_dual

Modified src/order/bounded_lattice.lean

added theorem bot_ne_top

added theorem top_ne_bot

Modified src/order/order_dual.lean

Modified src/ring_theory/ideal/basic.lean

modified def ideal.is_maximal