Theorem IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add

Modification history