Theorem Submodule.eq_starProjection_of_eq_submodule

Modification history