src/HOL/Library/Formal_Power_Series.thy

   finally have "(a*b) $ (i+j) \<noteq> 0" .
   then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast
 qed
 
 instance fps :: (idom) idom ..
+
+instantiation fps :: (comm_ring_1) number_ring
+begin
+definition number_of_fps_def: "(number_of k::'a fps) = of_int k"
+
+instance 
+by (intro_classes, rule number_of_fps_def)
+end
 
 subsection{* Inverses of formal power series *}
 
 declare setsum_cong[fundef_cong]