Theorem Submodule.map_equivMapOfInjective_symm_apply

Modification history