Theorem IsLocalRing.surjective_units_map_of_local_ringHom

Modification history