Theorem exists_associated_pow_of_mul_eq_pow

Modification history