Theorem Submodule.prodEquivOfIsCompl_symm_apply_right

Modification history