Theorem Submodule.orthogonalProjection_eq_linearProjOfIsCompl

Modification history