Theorem LocalRing.isUnit_or_isUnit_of_isUnit_add

Modification history