chore: fix pochhammer names (#7161)

those got somehow lost in the merges... Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Sep 15, 2023 · 20fb818 · 20fb818
1 parent 967f361
commit 20fb818
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
@@ -66,7 +66,7 @@ theorem ascPochhammer_succ_left (n : ℕ) :
   by rw [ascPochhammer]
 #align pochhammer_succ_left ascPochhammer_succ_left
 
-theorem monic_pochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] :
+theorem monic_ascPochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] :
     Monic <| ascPochhammer S n := by
   induction' n with n hn
   · simp
@@ -180,7 +180,7 @@ theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
 #align pochhammer_nat_eq_desc_factorial ascPochhammer_nat_eq_descFactorial
 
 @[simp]
-theorem pochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
+theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
     (ascPochhammer S n).natDegree = n := by
   induction' n with n hn
   · simp
@@ -356,13 +356,13 @@ theorem descPochhammer_mul (n m : ℕ) :
   · rw [descPochhammer_succ_right, Polynomial.mul_X_sub_int_cast_comp, ← mul_assoc, ih,
       Nat.succ_eq_add_one, ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
 
-theorem descPochhammer_int_eq_ascFactorial (n : ℕ) :
+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_ascFactorial n t]
+    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]
@@ -372,9 +372,9 @@ theorem descPochhammer_int_eq_ascFactorial (n : ℕ) :
     · left
       exact (Int.ofNat_sub <| not_lt.mp h).symm
 
-theorem Pochhammer_int_eq_descFactorial (a b : ℕ) :
+theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
     (descPochhammer ℤ b).eval (a + b : ℤ) = a.ascFactorial b := by
-  rw [← Nat.cast_add, descPochhammer_int_eq_ascFactorial (a + b) b,
+  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b,
       Nat.add_descFactorial_eq_ascFactorial]
 
 end Ring