Theorem Submodule.linearProjOfIsCompl_idempotent

Modification history