Factors_of_Binomial_Coefficient
Provedbinomial-coefficientscombinatoricsproofwiki
k * C(n, k) = n * C(n-1, k-1).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Factors_of_Binomial_Coefficient (n k : ℕ) (hk : 0 < k) (hkn : k ≤ n) : k * Nat.choose n k = n * Nat.choose (n - 1) (k - 1) := by sorry
Source