mathlib

591c34b6 - refactor(linear_algebra/basic): move the lattice structure to its own file (#6767)

refactor(linear_algebra/basic): move the lattice structure to its own file (#6767) The entire lattice structure is thoroughly uninteresting. By moving it to its own shorter file, it should be easier to unify with the lattice of `submonoid` I'd hope in future we can generate this automatically for any `subobject A` with an injection into `set A`.