Theorem IsDedekindDomainInv.inv_mul_eq_one

Modification history