src/HOL/Number_Theory/Binomial.thy
changeset 35644 d20cf282342e
parent 32479 521cc9bf2958
child 35731 1bdaa24fb56d
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
    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