mathlib

f548db40 - feat(linear_algebra/affine_space): lattice structure on affine subspaces (#3288)

feat(linear_algebra/affine_space): lattice structure on affine subspaces (#3288) Define a `complete_lattice` instance on affine subspaces of an affine space, and prove a few basic lemmas relating to it. (There are plenty more things that could be proved about it, that I think can reasonably be added later.)