X_i divides f if f=0 when X_i=0

Stream: Is there code for X?

[Kevin Buzzard]

The students at Imperial working on Newton's symmetric function theorem asked me on Thursday whether we had something like this:

import data.mv_polynomial.comm_ring

lemma mv_polynomial.dvd_iff (σ : Type*)  [fintype σ] [decidable_eq σ] (R : Type*) [comm_ring R]
  (p : mv_polynomial σ R) (i : σ) :
  mv_polynomial.eval₂ mv_polynomial.C (λ t, if t = i then 0 else mv_polynomial.X t) p = 0 →
  mv_polynomial.X i ∣ p :=
begin
  sorry
end

I've had a look through the mv_polynomial API and I can't find anything which looks helpful. A result of this nature is available for single-variable polynomials but it would probably be quite a kerfuffle to apply it. I must confess I am half-skeptical that this result really is in a sufficiently useful form for it to be usable elsewhere, but at the end of the day we should still be able to prove it relatively straightforwardly. The paper proof is something like: "write $p=r+X_iq$ where $r$ is the monomials in $p$ which don't mention $X_i$, and now show that setting $X_i=0$ in $p$ just gives you $q$, so $q=0$". Do we have the decomposition of a multivariable polynomial $p$ as a polynomial in one of its variables, or even just $p=r+X_iq$? It seems to me that /ₘ only exists for single-variable polynomials...

[Eric Wieser]

I think "write $p = r + X_i q$" is something like docs#polynomial.div_X?

[Eric Wieser]

Ah, I tried to do this in #15905

[Eric Wieser]

The result there is

lemma div_monomial_add_mod_monomial_single (x : mv_polynomial σ R) (i : σ) :
  X i * div_monomial (finsupp.single i 1) x + mod_monomial (finsupp.single i 1) x = x :=
x.div_of_add_mod_of _

[Kevin Buzzard]

Eric Wieser said:

I think "write $p = r + X_i q$" is something like docs#polynomial.div_X?

yeah exactly but it's mv_polynomials, hence the problems.

[Kevin Buzzard]

Eric Wieser said:

Ah, I tried to do this in https://github.com/leanprover-community/mathlib4/pull/2632

I think you might have posted the wrong URL?

[Eric Wieser]

Oops, #15905

[Kevin Buzzard]

Yes, a combination of div_monomial_add_mod_monomial_single and an assertion of the form mod_monomial (finsupp.single i 1) p = mv_polynomial.eval₂ mv_polynomial.C (λ t, if t = i then 0 else mv_polynomial.X t) p will do it. It's annoying that this sort of thing is still such a struggle.

[Eric Wieser]

I think I just forgot about that PR because of my internship

[Kevin Buzzard]

Kevin Buzzard said:

an assertion of the form mod_monomial (finsupp.single i 1) p = mv_polynomial.eval₂ mv_polynomial.C (λ t, if t = i then 0 else mv_polynomial.X t) p

This is also equal to (finset.filter (λ (f : σ →₀ ℕ), ⇑f i = 0) p.support).sum (λ (x : σ →₀ ℕ), ⇑(mv_polynomial.monomial x) (mv_polynomial.coeff x p))

[Eric Wieser]

@Damiano Testa had a related PR #15983, and I think we were half way through working out the set of assumptions that worked for both applications

[Eric Wieser]

#15905 is now merged, docs#mv_polynomial.div_monomial_add_mod_monomial_single will exist soon