exact mul_dvd_mul_left _ (Finset.dvd_sum (fun x hx ↦ dvd_mul_of_dvd_left
  (dvd_mul_of_dvd_left (dvd_pow (dvd_mul_right _ _) (Finset.mem_Ioo.mp hx).1.ne.symm) _) _))
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ ↑p * C a ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
no goals