Theorems · Theorem · field theory

Polynomial.dvd_term_of_dvd_eval_of_dvd_terms

∀ {S : Type v} [inst : CommRing S] {z p : S} {f : Polynomial S} (i : ℕ),
  p ∣ Polynomial.eval z f → (∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j) → p ∣ f.coeff i * z ^ i

Defined in

Mathlib.Algebra.Polynomial.AlgebraMap

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing