Theorem Submodule.IsCompl.projection_add_projection_eq_self

Modification history