dvd_iff_content_dvd_content_and_primPart_dvd_primPart

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_iff_content_dvd_content_and_primPart_dvd_primPart {p q : R[X]} (hq : q ≠ 0) :
    p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart :=
  by
  constructor
  · rintro ⟨r, rfl⟩
    rw [content_mul, p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]
    exact ⟨dvd_mul_right .., dvd_mul_of_dvd_left p.primPart_dvd _⟩
  · rintro ⟨h₁, h₂⟩
    rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
    gcongr

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