Theorem Module.End.IsSemisimple.of_mem_adjoin_singleton

Modification history