Theorem Submodule.starProjection_mem_subspace_eq_self

Modification history