Theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add

Modification history