rw [map_mul, map_natCast]
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
⊢ C (↑p * a) ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
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)