mathlib

42eb7f2d - feat(linear_algebra/basis): shows the lattice of submodules of a module over a division ring is atomistic (#14883)

feat(linear_algebra/basis): shows the lattice of submodules of a module over a division ring is atomistic (#14883) This PR shows that the lattice of submodules of a module over a division ring is atomistic, and that the atoms of this lattice are the spans of nonzero elements.