Theorem Submodule.IsOrtho.starProjection_comp_starProjection

Modification history