Theorem Submodule.linearProjOfIsCompl_eq_self_iff

Modification history