Modular lattice of linear subspaces

The subspaces {vspace vT} of a vector space vT (defined in vector.v) seem to form a lattice. A Wikipedia article says that "the operations intersection and sum make the set of all (linear) subspaces a bounded modular lattice". So we may apply the lattice theory to reason about linear subspaces by defining this lattice structure instance. Also, the modular lattice structures are intermediate ones between (tb)LatticeType and (tb)DistrLatticeType. So it would be nice to have them in order.v. Does this make sense? Is there any good literature on this topic?

These lattices also seem to be complemented and graded but non-distributive. There might be so many missing structures.

Yes, we should definitely provide the lattice structure at some point. It makes sense. I do not of any literature in particular, this is folklore... most book simply mention the lattice structure by the way...

Since the complement of linear subspaces is not unique, I am not sure whether we should have such complemented non-distributive lattice structures anymore. Declaring the canonical tbLatticeType of them and deprecating the lemmas for linear subspaces in vector.v that are already proved for lattices seems rather reasonable to me for now.

Since the complement of linear subspaces is not unique, I am not sure whether we should have such complemented non-distributive lattice structures anymore.

The orthogonal complement defined relatively to the canonical inner product induced by the canonical basis is unique though.