dvd_primPart_iff_dvd — Mathlib

English

For primitive p and nonzero q, p divides q.primPart if and only if p divides q.

Русский

Для примитивного p и ненулевого q выполняется: p делит q.primPart тогда и только тогда, когда p делит q.

LaTeX

$$$p.IsPrimitive \land q \neq 0 \Rightarrow p \mid q.primPart \iff p \mid q$$$

Lean4

theorem dvd_primPart_iff_dvd {p q : R[X]} (hp : p.IsPrimitive) (hq : q ≠ 0) : p ∣ q.primPart ↔ p ∣ q :=
  by
  refine ⟨fun h => h.trans (Dvd.intro_left _ q.eq_C_content_mul_primPart.symm), fun h => ?_⟩
  rcases h with ⟨r, rfl⟩
  apply Dvd.intro _
  rw [primPart_mul hq, hp.primPart_eq]

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