Re: [isabelle] newbie: Binomial extensions



gbinomial (syntax: "n gchoose k") is already that generalisation. It
works for pretty much anything as the first argument, but the second
argument must be a natural numbers. Seeing as we have the Gamma and Beta
functions in HOL-Analysis, one could also easily extend it to complex
numbers.

I'm not sure what field extensions have to do with any of this. What
field are you talking about? What do you want to extend it to? What does
that have to do with binomial coefficients?

Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.