Vandermonde

Statistics

Metric	Count
Definitions	0
Theorems `add_choose_eq`, `sum_range_choose_sq`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`add_choose_eq` 📖	mathematical	—	`choose` `Finset.sum` `instAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	`Polynomial.coeff_X_add_one_pow` `cast_id` `pow_add` `Polynomial.coeff_mul` `Finset.sum_congr`
`sum_range_choose_sq` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `instMonoid` `choose`	—	`instAtLeastTwoHAddOfNat` `two_mul` `add_choose_eq` `Finset.sum_congr` `choose_symm` `Finset.mem_range_succ_iff` `sq`

---