Theorem Submodule.eq_starProjection_of_mem_orthogonal

Modification history