vandermonde): Vandermonde's identity for binomial coefficients (#8992)

Commit

4 years ago

feat(data/nat/choose/vandermonde): Vandermonde's identity for binomial coefficients (#8992) I place this identity in a new file because the current proof depends on `polynomial`.

Author

jcommelin

Parents

9fc45d81

mathlib3 0a94b29f - feat(data/nat/choose/vandermonde): Vandermonde's identity for binomial coefficients (#8992)

mathlib3
0a94b29f - feat(data/nat/choose/vandermonde): Vandermonde's identity for binomial coefficients (#8992)