Theorem isLocalRingHom_of_exists_map_ne_one

Modification history