Theorem Submodule.linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl

Modification history