Theorem Submodule.isIdempotentElem_subtype_comp_linearProjOfIsCompl

Modification history