Theorem IsUnit.isNilpotent_mul_unit_of_commute_iff

Modification history