# HG changeset patch # User haftmann # Date 1534941178 0 # Node ID 248e1678ce556c3b7878d6d2bd5cb1aed454655f # Parent 8ff34c1ad580630a640b0101e5e21ee90c709c18 more theorems on fact diff -r 8ff34c1ad580 -r 248e1678ce55 src/HOL/Factorial.thy --- a/src/HOL/Factorial.thy Wed Aug 22 12:32:58 2018 +0000 +++ b/src/HOL/Factorial.thy Wed Aug 22 12:32:58 2018 +0000 @@ -174,12 +174,30 @@ by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono) qed +lemma prod_Suc_fact: "prod Suc {0.. = prod Suc (insert 0 {Suc 0.. \Evaluation for specific numerals\ by (metis fact_Suc numeral_eq_Suc of_nat_numeral) - subsection \Pochhammer's symbol: generalized rising factorial\ text \See \<^url>\https://en.wikipedia.org/wiki/Pochhammer_symbol\.\