mathlib

030107f6 - feat(order/compactly_generated): A compactly-generated modular lattice is complemented iff atomistic (#6071)

feat(order/compactly_generated): A compactly-generated modular lattice is complemented iff atomistic (#6071) Shows that a compactly-generated modular lattice is complemented iff it is atomistic Proves extra lemmas about atomistic or compactly-generated lattices Proves extra lemmas about `complete_lattice.independent` Fix the name of `is_modular_lattice.sup_inf_sup_assoc` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>