Theorem Submodule.torsionBySet_le_torsionBySet_of_subset

Modification history