Vector space as sum of subspaces

Stream: Is there code for X?

[Andy Heald]

Is there code for the fact that if U is a subspace of V then there exists U' such that

$$U \oplus U' = V$$

[Adam Topaz]

I think we have this...

[Adam Topaz]

docs#Submodule.exists_isCompl

[Adam Topaz]

along with docs#Submodule.prodEquivOfIsCompl

[Adam Topaz]

I guess ComplementedLattice.exists_isCompl is what one should use.