p divided q iff p divides k * q for nonzero k (polynomials)

Stream: Is there code for X?

[Ilmārs Cīrulis]

How can one prove this? Is there something in Mathlib, maybe? (I didn't find yet.)

import Mathlib

open Polynomial

theorem thm (p q: ℤ[X]) (Hp: Monic p) (k: ℤ) (Hk: k ≠ 0):
    p ∣ C k * q ↔ p ∣ q := by
  sorry

[Yaël Dillies]

This is a direct consequence of docs#IsUnit.dvd_mul_left, docs#Polynomial.isUnit_C

[Yaël Dillies]

Hmm, it would be if ℤ was a field

[Ruben Van de Velde]

Is it true?

[Junyan Xu]

One possible proof:

import Mathlib.Algebra.GCDMonoid.Nat
import Mathlib.RingTheory.Polynomial.Content

open Polynomial in
theorem thm (p q : ℤ[X]) (hp : Monic p) (k : ℤ) (hk : k ≠ 0):
    p ∣ C k * q ↔ p ∣ q := by
  obtain rfl | hq := eq_or_ne q 0; · simp
  have := mul_ne_zero (C_ne_zero.mpr hk) hq
  rw [← hp.isPrimitive.dvd_primPart_iff_dvd this, ← hp.isPrimitive.dvd_primPart_iff_dvd hq,
    primPart_mul this, (isUnit_primPart_C _).dvd_mul_left]

[Ilmārs Cīrulis]

Thank you!