pow_X_dvd_iff

Stream: Is there code for X?

[Filippo A. E. Nuccio]

I was unable to find the (actually quite easy to prove)

theorem pow_X_dvd_iff {α : Type } [comm_semiring α] {f : α[X]} {n : ℕ} :
  X^n ∣ f ↔ ∀ d < n, f.coeff d = 0 :=

although there is the

theorem X_dvd_iff {α : Type u} [comm_semiring α] {f : α[X]} : X ∣ f ↔ f.coeff 0 = 0 :=

Am I missing it?

[Anne Baanen]

I don't recall ever seeing anything like that and I can't find it either. So I'd say go ahead and add this! (Nitpick: I'd call it polynomial.X_pow_dvd_iff, putting the infix operator after its left argument).

[Filippo A. E. Nuccio]

OK, I'll open the PR straight away.

[Filippo A. E. Nuccio]

Done, #18528

[Eric Wieser]

Can you add the multivariate one too?

[Filippo A. E. Nuccio]

Since the previous PR has been delegated, should I accept that one first and open a new one with the mv stuff? Especially because even the basic var_dvd_iff (where the power of a variable is $1$) seems missing.

[Anne Baanen]

You can go either way: you can re-request a review or merge this and then start a new mv_polynomial PR (which I'm happy to review).

[Filippo A. E. Nuccio]

OK, I will then go for the second option, since I am also working on another project where I only need the single-variable lemma, and at least that one can advance. I wait for CIto finish, at any rate.