71 |
71 |
72 lemma transfer_nat_int_binomial_closure: |
72 lemma transfer_nat_int_binomial_closure: |
73 "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0" |
73 "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0" |
74 by (auto simp add: binomial_int_def) |
74 by (auto simp add: binomial_int_def) |
75 |
75 |
76 declare TransferMorphism_nat_int[transfer add return: |
76 declare transfer_morphism_nat_int[transfer add return: |
77 transfer_nat_int_binomial transfer_nat_int_binomial_closure] |
77 transfer_nat_int_binomial transfer_nat_int_binomial_closure] |
78 |
78 |
79 lemma transfer_int_nat_binomial: |
79 lemma transfer_int_nat_binomial: |
80 "binomial (int n) (int k) = int (binomial n k)" |
80 "binomial (int n) (int k) = int (binomial n k)" |
81 unfolding fact_int_def binomial_int_def by auto |
81 unfolding fact_int_def binomial_int_def by auto |
82 |
82 |
83 lemma transfer_int_nat_binomial_closure: |
83 lemma transfer_int_nat_binomial_closure: |
84 "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0" |
84 "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0" |
85 by (auto simp add: binomial_int_def) |
85 by (auto simp add: binomial_int_def) |
86 |
86 |
87 declare TransferMorphism_int_nat[transfer add return: |
87 declare transfer_morphism_int_nat[transfer add return: |
88 transfer_int_nat_binomial transfer_int_nat_binomial_closure] |
88 transfer_int_nat_binomial transfer_int_nat_binomial_closure] |
89 |
89 |
90 |
90 |
91 subsection {* Binomial coefficients *} |
91 subsection {* Binomial coefficients *} |
92 |
92 |