chore(Data/Nat/{Factorial, Choose}/Cast): move lemmas about Polynomial (#30745)

The remaining lemmas in the files are unrelated to `ascPochhammer` and `descPochhammer`. This significantly reduces the imports.

Author: astrainfinita

Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

@@ -6,7 +6,6 @@ Authors: Mitchell Horner
 import Mathlib.Algebra.BigOperators.Field
 import Mathlib.Analysis.Convex.Deriv
 import Mathlib.Analysis.Convex.Piecewise
-import Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Analysis.Convex.Jensen
 
 /-!

Mathlib/Data/Nat/Choose/Cast.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Data.Nat.Choose.Basic
 import Mathlib.Data.Nat.Factorial.Cast
 
@@ -23,31 +25,21 @@ section DivisionSemiring
 variable [DivisionSemiring K] [CharZero K]
 
 theorem cast_choose {a b : ℕ} (h : a ≤ b) : (b.choose a : K) = b ! / (a ! * (b - a)!) := by
-  have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (by positivity)
+  have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_pos _).ne'
   rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
   rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
 
 theorem cast_add_choose {a b : ℕ} : ((a + b).choose a : K) = (a + b)! / (a ! * b !) := by
-  rw [cast_choose K (_root_.le_add_right le_rfl), add_tsub_cancel_left]
-
-theorem cast_choose_eq_ascPochhammer_div (a b : ℕ) :
-    (a.choose b : K) = (ascPochhammer K b).eval ↑(a - (b - 1)) / b ! := by
-  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
-    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
+  rw [cast_choose K (le_add_right _ _), Nat.add_sub_cancel_left]
 
 end DivisionSemiring
 
 section DivisionRing
-variable [DivisionRing K] [CharZero K]
-
-theorem cast_choose_eq_descPochhammer_div (a b : ℕ) :
-    (a.choose b : K) = (descPochhammer K b).eval ↑a / b ! := by
-  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
-    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
+variable [DivisionRing K] [NeZero (2 : K)]
 
 theorem cast_choose_two (a : ℕ) : (a.choose 2 : K) = a * (a - 1) / 2 := by
   rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
-    cast_mul, cast_two, eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]
+    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]
 
 end DivisionRing
 end Nat

Mathlib/Data/Nat/Factorial/Cast.lean

@@ -3,7 +3,8 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.RingTheory.Polynomial.Pochhammer
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Data.Nat.Factorial.Basic
 
 /-!
 # Cast of factorials
@@ -24,43 +25,17 @@ variable (S : Type*)
 
 namespace Nat
 
-section Semiring
-
-variable [Semiring S] (a b : ℕ)
-
-theorem cast_ascFactorial : a.ascFactorial b = (ascPochhammer S b).eval (a : S) := by
-  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]
-
-theorem cast_descFactorial :
-    a.descFactorial b = (ascPochhammer S b).eval (a - (b - 1) : S) := by
-  rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]
-  induction b with
-  | zero => simp
-  | succ b =>
-    simp_rw [add_succ, Nat.add_one_sub_one]
-    obtain h | h := le_total a b
-    · rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
-      rw [tsub_eq_zero_iff_le.mpr h, zero_add]
-    · rw [tsub_add_cancel_of_le h]
-
-theorem cast_factorial : (a ! : S) = (ascPochhammer S a).eval 1 := by
-  rw [← one_ascFactorial, cast_ascFactorial, cast_one]
-
-end Semiring
-
 section Ring
 
 variable [Ring S] (a b : ℕ)
 
 /-- Convenience lemma. The `a - 1` is not using truncated subtraction, as opposed to the definition
 of `Nat.descFactorial` as a natural. -/
 theorem cast_descFactorial_two : (a.descFactorial 2 : S) = a * (a - 1) := by
-  rw [cast_descFactorial]
+  rw [descFactorial]
   cases a
   · simp
-  · rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel_right, ascPochhammer_succ_right,
-      ascPochhammer_one, Polynomial.X_mul, Polynomial.eval_mul_X, Polynomial.eval_add,
-      Polynomial.eval_X, cast_one, Polynomial.eval_one]
+  · simp [mul_add, add_mul]
 
 end Ring
 

Mathlib/RingTheory/Polynomial/Pochhammer.lean

@@ -228,6 +228,29 @@ theorem ascPochhammer_eval_succ (r n : ℕ) :
     (n + r) * (ascPochhammer S r).eval (n : S) :=
   mod_cast congr_arg Nat.cast (ascPochhammer_nat_eval_succ r n)
 
+namespace Nat
+variable (a b : ℕ)
+
+theorem cast_ascFactorial : a.ascFactorial b = (ascPochhammer S b).eval (a : S) := by
+  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]
+
+theorem cast_descFactorial :
+    a.descFactorial b = (ascPochhammer S b).eval (a - (b - 1) : S) := by
+  rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]
+  induction b with
+  | zero => simp
+  | succ b =>
+    simp_rw [add_succ, Nat.add_one_sub_one]
+    obtain h | h := le_total a b
+    · rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
+      rw [tsub_eq_zero_iff_le.mpr h, zero_add]
+    · rw [tsub_add_cancel_of_le h]
+
+theorem cast_factorial : (a ! : S) = (ascPochhammer S a).eval 1 := by
+  rw [← one_ascFactorial, cast_ascFactorial, cast_one]
+
+end Nat
+
 end Factorial
 
 section Ring
@@ -484,3 +507,27 @@ theorem monotoneOn_descPochhammer_eval (n : ℕ) :
       (sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)
 
 end StrictOrderedRing
+
+variable (K : Type*)
+
+namespace Nat
+section DivisionSemiring
+variable [DivisionSemiring K] [CharZero K]
+
+theorem cast_choose_eq_ascPochhammer_div (a b : ℕ) :
+    (a.choose b : K) = (ascPochhammer K b).eval ↑(a - (b - 1)) / b ! := by
+  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
+    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
+
+end DivisionSemiring
+
+section DivisionRing
+variable [DivisionRing K] [CharZero K]
+
+theorem cast_choose_eq_descPochhammer_div (a b : ℕ) :
+    (a.choose b : K) = (descPochhammer K b).eval ↑a / b ! := by
+  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
+    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
+
+end DivisionRing
+end Nat