R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y✝ x y p : R
h : ↑(Ideal.Quotient.mk (span {p})) x = ↑(Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i in range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y✝ x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i in range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
rw [← mem_span_singleton, ← Ideal.Quotient.eq] at h
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y✝ x y p : R
h : ↑(Ideal.Quotient.mk (span {p})) x = ↑(Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i in range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
simp only [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, h, geom_sum₂_self,
  _root_.map_mul, map_pow, map_natCast]