Polynomial

Stream: new members

[Wouter Smeenk]

I am trying to prove something similar to this (the polynomial is multivariate and more complex):

variable {x : ℤ}
example : 2 - x + x ^ 2 ≠ 0 := by
  sorry

I found Polynomial.IsEisensteinAt.irreducible, but In order to use I need the formula to be of the type Polynomial. How do I achive this? Also can you apply this irreducible lemma to MvPolynomial?

[Damiano Testa]

What you wrote is not technically a Polynomial: this is how your example could be proved using actual Polynomials

import Mathlib

open Polynomial

variable {x : ℤ}

example : (2 - X + X ^ 2 : ℤ[X]) ≠ 0 := by
  apply_fun (coeff · 0)
  simp

[Damiano Testa]

MvPolynomial requires a bit of extra setup, so providing a #mwe would help.

[Wouter Smeenk]

Oke thanks for that example/proof. But what if 2 - x + x ^ 2 ≠ 0 appears in the goal. How would you go about converting Polynomial in order to prove it?

[Damiano Testa]

I may be misunderstanding, but the Polynomial (2 - X + X ^ 2 : ℤ[X]) being non-zero does not imply that your expression 2 - x + x ^ 2 is non-zero.

[Damiano Testa]

(I am pointing out something very silly: the polynomial X is non-zero, but x does vanish...)

[Damiano Testa]

I think that providing a #mwe will help disambiguate your question.

[Damiano Testa]

Btw, the proposal of having a tactic to convert a "polynomial expression" into an actual Polynomial arose already, but I think that no one ended up writing the tactic.

[Yaël Dillies]

Damiano Testa said:

(I am pointing out something very silly: the polynomial X is non-zero, but x does vanish...)

Damiano, you misunderstood Wouter's goal

[Wouter Smeenk]

Damiano Testa said:

I may be misunderstanding, but the Polynomial (2 - X + X ^ 2 : ℤ[X]) being non-zero does not imply that your expression 2 - x + x ^ 2 is non-zero.

I guess I don't really understand why this is not true. I also do not really understand what you mean by 'but x does vanish.

[Yaël Dillies]

2 - X + X ^ 2 being irreducible over ℤ implies that 2 - x + x ^ 2 ≠ 0 for all x : ℤ

[Riccardo Brasca]

What Damiano is saying is that if P is a polynomial, then P ≠ 0 does not imply that P(x) ≠ 0 for all x, this still depends on x.

[Yaël Dillies]

Yes, but that's not what Wouter asked for :thinking:

[Yaël Dillies]

Wouter wants to prove that the polynomial is irreducible, hence has no integer root

[Michael Stoll]

Anyway, the polynomial is not an Eisenstein polynomial.

[Riccardo Brasca]

In the Lean code there is 2 - x + x ^ 2 ≠ 0, where (x : ℤ), this is why we are asking for a #mwe.

[Michael Stoll]

It is still irreducible, because its discriminant $-7$ is not a square in $\mathbb Z$.

[Michael Stoll]

One could just reduce mod 3 in this case.

[Michael Stoll]

import Mathlib

lemma aux : ∀ a : ZMod 3, 2 - a + a ^ 2 ≠ 0 := by decide

example (x : ℤ) : 2 - x + x ^ 2 ≠ 0 := by
  intro h
  apply_fun ((↑) : ℤ → ZMod 3) at h
  push_cast at h
  exact aux _ h

[Kevin Buzzard]

Oh very nice!

[Wouter Smeenk]

It is a bit hard to provide a #mwe. I guess my original example was not that good. But this trick with ZMod 3 helps. Thanks!