Theorem IsLocalRing.isUnit_or_isUnit_one_sub_self

Modification history