src/HOL/Library/Poly_Mapping.thy

   using finite_cmul_nonzero [of c a]
   by (metis lookup_frag_cmul mult_zero_right not_in_keys_iff_lookup_eq_zero subsetI)
   
 
 lemma keys_cmul_iff [iff]: "i \<in> Poly_Mapping.keys (frag_cmul c x) \<longleftrightarrow> i \<in> Poly_Mapping.keys x \<and> c \<noteq> 0"
-  apply (auto simp: )
+  apply auto
   apply (meson subsetD keys_cmul)
   by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
 
 lemma keys_minus [simp]: "Poly_Mapping.keys(-a) = Poly_Mapping.keys a"
   by (metis (no_types, opaque_lifting) in_keys_iff lookup_uminus neg_equal_0_iff_equal subsetI subset_antisym)