Theorem Submodule.IsPrincipal.span_singleton_generator

Modification history