choose neg

Stream: lean4

[oishi]

how can i proof this? since (0-1) is Nat, in lean4, this will be 0-1 = 0. how can i proof this right?

lemma choose_neg (n:ℕ) : n.choose (0 - 1) = (0:ℝ) := by sorry

[Julian Berman]

Have a look at #backticks which will help you format your message for Zulip.

As for your question, it's false -- n choose 0 is 1, not 0:

lemma choose_neg (n:ℕ) : n.choose (0 - 1) = (1:ℝ) := by norm_num

[oishi]

Julian Berman said:

Have a look at #backticks which will help you format your message for Zulip.

As for your question, it's false -- n choose 0 is 1, not 0:

lemma choose_neg (n:ℕ) : n.choose (0 - 1) = (1:ℝ) := by norm_num

Thanks. However, I want to proof n.choose (-1) actually.
The "choose" is defined on the set of natural numbers, and I would like to know how it can be extended to integers. Should choosing a negative number be equal to 0?

[Johan Commelin]

This discussion seems relevant: #Is there code for X? > Choose on integer

[oishi]

That's helpful. Thanks a lot!!!