feat: Define general binomial coefficients (Ring.choose) (#9719)

We define generalized binomial coefficients, and prove a couple basic properties. In particular, we show that
multiplication by a suitable factorial yields a descending Pochhammer evaluation.  We also show that casting `Nat.choose` is the same as taking `Ring.choose` of a natural number cast.  To prove these, we add some results about polynomial evaluation.

Author: ScottCarnahan

Mathlib/Data/Nat/Factorial/SuperFactorial.lean

@@ -106,7 +106,7 @@ private theorem matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose {n : ℕ} (v
     (∏ i : Fin n, Nat.factorial i) *
       (Matrix.of (fun (i j : Fin n) => (Nat.choose (v i) (j : ℕ) : ℤ))).det := by
   convert Matrix.det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)):ℤ)) _
-  · rw [Matrix.of_apply, descPochhammer_int_eq_descFactorial _ _]
+  · rw [Matrix.of_apply, descPochhammer_eval_eq_descFactorial ℤ _ _]
     congr
     exact Nat.descFactorial_eq_factorial_mul_choose _ _
   · rw [Nat.cast_prod]

Mathlib/Data/Polynomial/Eval.lean

@@ -1071,6 +1071,31 @@ theorem iterate_comp_eval₂ (k : ℕ) (t : S) :
 
 end
 
+section Algebra
+
+variable [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p q : R[X])
+
+@[simp]
+theorem eval₂_mul' :
+    (p * q).eval₂ (algebraMap R S) x = p.eval₂ (algebraMap R S) x * q.eval₂ (algebraMap R S) x := by
+  exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x
+
+@[simp]
+theorem eval₂_pow' (n : ℕ) :
+    (p ^ n).eval₂ (algebraMap R S) x = (p.eval₂ (algebraMap R S) x) ^ n := by
+  induction n with
+  | zero => simp only [Nat.zero_eq, pow_zero, eval₂_one]
+  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]
+
+@[simp]
+theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) =
+    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p := by
+  induction p using Polynomial.induction_on' with
+    | h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
+    | h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
+
+end Algebra
+
 section
 
 variable [CommSemiring R] {p q : R[X]} {x : R} [CommSemiring S] (f : R →+* S)

Mathlib/RingTheory/Binomial.lean

@@ -30,13 +30,14 @@ Pochhammer polynomial `X(X+1)⋯(X+(k-1))` at any element is divisible by `k!`.
 ## TODO
 
 * Replace `Nat.multichoose` with `Ring.multichoose`.
-* `Ring.choose` for binomial rings.
-* Generalize to the power-associative case, when power-associativity is implemented.
+* Generalize from `Semiring` to `AddCommMonoid` with `Pow R ℕ` using `smeval`.
 
 -/
 
 open Function
 
+section Multichoose
+
 /-- A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
 suitable factorials.  We define this notion for semirings, but retain the ring name.  We introduce
 `Ring.multichoose` as the uniquely defined quotient. -/
@@ -49,8 +50,6 @@ class BinomialRing (R : Type*) [Semiring R] where
   factorial_nsmul_multichoose (r : R) (n : ℕ) :
     n.factorial • multichoose r n = Polynomial.eval r (ascPochhammer R n)
 
-section Binomial
-
 namespace Ring
 
 variable {R : Type*} [Semiring R] [BinomialRing R]
@@ -67,7 +66,7 @@ def multichoose (r : R) (n : ℕ) : R := BinomialRing.multichoose r n
 theorem multichoose_eq_multichoose (r : R) (n : ℕ) :
     BinomialRing.multichoose r n = multichoose r n := rfl
 
-theorem factorial_nsmul_multichoose_eq_eval_ascPochhammer (r : R) (n : ℕ) :
+theorem factorial_nsmul_multichoose_eq_ascPochhammer (r : R) (n : ℕ) :
     n.factorial • multichoose r n = Polynomial.eval r (ascPochhammer R n) :=
   BinomialRing.factorial_nsmul_multichoose r n
 
@@ -78,7 +77,7 @@ instance Nat.instBinomialRing : BinomialRing ℕ where
   multichoose := Nat.multichoose
   factorial_nsmul_multichoose r n := by
     rw [Nat.multichoose_eq, smul_eq_mul, ← Nat.descFactorial_eq_factorial_mul_choose,
-    ascPochhammer_nat_eq_descFactorial]
+      ascPochhammer_nat_eq_descFactorial]
 
 /-- The multichoose function for integers. -/
 def Int.multichoose (n : ℤ) (k : ℕ) : ℤ :=
@@ -98,7 +97,31 @@ instance Int.instBinomialRing : BinomialRing ℤ where
         ascPochhammer_eval_cast]
     | negSucc n =>
       rw [mul_comm, mul_assoc, ← Nat.cast_mul, mul_comm _ (k.factorial),
-        ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_int_eq_descFactorial,
+        ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_eval_eq_descFactorial,
         ← Int.neg_ofNat_succ, ascPochhammer_eval_neg_eq_descPochhammer]
 
-end Binomial
+end Multichoose
+
+section Choose
+
+namespace Ring
+
+variable {R : Type*} [Ring R] [BinomialRing R]
+
+/-- The binomial coefficient `choose r n` generalizes the natural number `choose` function,
+  interpreted in terms of choosing without replacement. -/
+def choose (r : R) (n : ℕ): R := multichoose (r - n + 1) n
+
+theorem descPochhammer_eq_factorial_smul_choose (r : R) (n : ℕ) :
+    Polynomial.eval r (descPochhammer R n) = n.factorial • choose r n := by
+  rw [choose, factorial_nsmul_multichoose_eq_ascPochhammer, descPochhammer_eval_eq_ascPochhammer]
+
+theorem choose_nat_cast (n k : ℕ) : choose (n : R) k = Nat.choose n k := by
+  refine nsmul_right_injective (Nat.factorial k) (Nat.factorial_ne_zero k) ?_
+  simp only
+  rw [← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
+  ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_eval_eq_descFactorial]
+
+end Ring
+
+end Choose

Mathlib/RingTheory/Polynomial/Pochhammer.lean

@@ -87,6 +87,17 @@ theorem ascPochhammer_map (f : S →+* T) (n : ℕ) :
   · simp [ih, ascPochhammer_succ_left, map_comp]
 #align pochhammer_map ascPochhammer_map
 
+theorem ascPochhammer_eval₂ (f : S →+* T) (n : ℕ) (t : T) :
+    (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t := by
+  rw [← ascPochhammer_map f]
+  exact eval_map f t
+
+theorem ascPochhammer_eval_comp {R : Type*} [CommSemiring R] (n : ℕ) (p : R[X]) [Algebra R S]
+    (x : S) : ((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x =
+    (ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x) := by
+  rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
+    ← map_comp, eval_map]
+
 end
 
 @[simp, norm_cast]
@@ -328,6 +339,16 @@ theorem descPochhammer_succ_comp_X_sub_one (n : ℕ) :
   rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, nat_cast_comp]
   ring
 
+theorem descPochhammer_eval_eq_ascPochhammer (r : R) (n : ℕ) :
+    (descPochhammer R n).eval r = (ascPochhammer R n).eval (r - n + 1) := by
+  induction n with
+  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
+  | succ n ih =>
+    rw [Nat.cast_succ, sub_add, add_sub_cancel, descPochhammer_succ_eval, ih,
+      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
+      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
+      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
+
 theorem descPochhammer_mul (n m : ℕ) :
     descPochhammer R n * (descPochhammer R m).comp (X - (n : R[X])) = descPochhammer R (n + m) := by
   induction' m with m ih
@@ -347,25 +368,20 @@ theorem ascPochhammer_eval_neg_eq_descPochhammer (r : R) : ∀ (k : ℕ),
       pow_add, pow_one, mul_assoc ((-1)^k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
       Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
 
-theorem descPochhammer_int_eq_descFactorial (n : ℕ) :
-    ∀ k, (descPochhammer ℤ k).eval (n : ℤ) = n.descFactorial k
-  | 0 => by
-    rw [descPochhammer_zero, eval_one, Nat.descFactorial_zero]
-    rfl
-  | t + 1 => by
-    rw [descPochhammer_succ_right, eval_mul, descPochhammer_int_eq_descFactorial n t]
-    simp only [eval_sub, eval_X, eval_nat_cast, Nat.descFactorial_succ, Nat.cast_mul,
-        Nat.descFactorial_eq_zero_iff_lt]
-    rw [mul_comm]
-    simp only [mul_eq_mul_right_iff, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt]
-    by_cases h : n < t
-    · tauto
-    · left
-      exact (Int.ofNat_sub <| not_lt.mp h).symm
+theorem descPochhammer_eval_eq_descFactorial (n k : ℕ) :
+    (descPochhammer R k).eval (n : R) = n.descFactorial k := by
+  induction k with
+  | zero => rw [descPochhammer_zero, eval_one, Nat.descFactorial_zero, Nat.cast_one]
+  | succ k ih =>
+    rw [descPochhammer_succ_right, Nat.descFactorial_succ, mul_sub, eval_sub, eval_mul_X,
+      ← Nat.cast_comm k, eval_nat_cast_mul, ← Nat.cast_comm n, ← sub_mul, ih]
+    by_cases h : n < k
+    rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero]
+    rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h]
 
 theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
     (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by
-  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b,
+  rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
     Nat.add_descFactorial_eq_ascFactorial]
 
 end Ring