mathlib

124aa163 - feat(order/modular_lattice): Modular lattices are lower modular (#17403)

feat(order/modular_lattice): Modular lattices are lower modular (#17403) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: D.M.H. van Gent <gentdmhvan@u0031838.vuw.leidenuniv.nl> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>