--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Feb 22 07:49:48 2021 +0000
@@ -1507,7 +1507,7 @@
assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
using finite_number_of_roots[OF assms]
unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
- by (simp add: multiset_def roots_def)
+ by (simp add: roots_def)
lemma (in domain) roots_mem_iff_is_root:
assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"