equal
deleted
inserted
replaced
184 of_nat_setsum [symmetric] |
184 of_nat_setsum [symmetric] |
185 of_nat_eq_iff of_nat_id) |
185 of_nat_eq_iff of_nat_id) |
186 |
186 |
187 subsection{* Pochhammer's symbol : generalized rising factorial *} |
187 subsection{* Pochhammer's symbol : generalized rising factorial *} |
188 |
188 |
189 text {* See \url{http://en.wikipedia.org/wiki/Pochhammer_symbol} *} |
189 text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *} |
190 |
190 |
191 definition "pochhammer (a::'a::comm_semiring_1) n = |
191 definition "pochhammer (a::'a::comm_semiring_1) n = |
192 (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})" |
192 (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})" |
193 |
193 |
194 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" |
194 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" |