binomial on integer

Stream: mathlib4

[Gaolei He]

I'm doing some binomial problems
I want to ask that does lean4 have define

$$\binom{n}{k}=0$$

when k < 0?
or in other words: how do we deal with negative numbers in binomial in lean4

[Kevin Buzzard]

Nat.choose : ℕ → ℕ → ℕ so your question doesn't even typecheck. In other words, Nat.choose by definition eats two natural numbers.

[Edward van de Meent]

there is also Ring.choose

[Edward van de Meent]

(which applies to integers too, afaict)

[Edward van de Meent]

actually nvm, that also only eats natural numbers

[Edward van de Meent]

do check out #Is there code for X? > Choose on integer for a similar question/conversation

[Notification Bot]

6 messages were moved here from #mathlib4 > question about Ico by Edward van de Meent.