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)"
```