--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Jan 21 11:02:27 2020 +0100
@@ -48,7 +48,7 @@
by (simp add: One_nat_def [symmetric] del: One_nat_def)
lemma is_nth_power_conv_multiplicity:
- fixes x :: "'a :: factorial_semiring"
+ fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}"
assumes "n > 0"
shows "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
proof (cases "x = 0")