equal
deleted
inserted
replaced
46 |
46 |
47 lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)" |
47 lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)" |
48 by (simp add: One_nat_def [symmetric] del: One_nat_def) |
48 by (simp add: One_nat_def [symmetric] del: One_nat_def) |
49 |
49 |
50 lemma is_nth_power_conv_multiplicity: |
50 lemma is_nth_power_conv_multiplicity: |
51 fixes x :: "'a :: factorial_semiring" |
51 fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}" |
52 assumes "n > 0" |
52 assumes "n > 0" |
53 shows "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)" |
53 shows "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)" |
54 proof (cases "x = 0") |
54 proof (cases "x = 0") |
55 case False |
55 case False |
56 show ?thesis |
56 show ?thesis |