dvd_content_iff_C_dvd — Mathlib

English

For a polynomial p and a ring element r, r divides p.content iff C r divides p.

Русский

Для полинома p и элемента кольца r: r делит p.content тогда и только тогда, когда C r делит p.

LaTeX

$$$$ r \\mid p.content \\iff C r \\mid p $$$$

Lean4

theorem dvd_content_iff_C_dvd {p : R[X]} {r : R} : r ∣ p.content ↔ C r ∣ p :=
  by
  rw [C_dvd_iff_dvd_coeff]
  constructor
  · intro h i
    apply h.trans (content_dvd_coeff _)
  · intro h
    rw [content, Finset.dvd_gcd_iff]
    intro i _
    apply h i

Похожие утверждения