Theorem Submodule.IsCompl.projection_eq_self_sub_projection

Modification history