src/HOL/Computational_Algebra/Formal_Power_Series.thy
changeset 68442 477b3f7067c9
parent 68072 493b818e8e10
child 68975 5ce4d117cea7
     1.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 14 10:51:12 2018 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 14 15:45:53 2018 +0200
     1.3 @@ -4601,7 +4601,7 @@
     1.4  
     1.5  subsection \<open>Hypergeometric series\<close>
     1.6  
     1.7 -definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) =
     1.8 +definition "fps_hypergeo as bs (c::'a::field_char_0) =
     1.9    Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
    1.10      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
    1.11  
    1.12 @@ -4686,11 +4686,11 @@
    1.13    by (simp add: fps_eq_iff fps_integral_def)
    1.14  
    1.15  lemma fps_hypergeo_minus_nat:
    1.16 -  "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
    1.17 +  "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::field_char_0) $ k =
    1.18      (if k \<le> n then
    1.19        pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
    1.20       else 0)"
    1.21 -  "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
    1.22 +  "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::field_char_0) $ k =
    1.23      (if k \<le> m then
    1.24        pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
    1.25       else 0)"