nonzero polynomials take on nonzero values

Stream: Is there code for X?

[Johan Commelin]

Do we have this? Or can we prove it in an easy manner?

import Mathlib.Data.Polynomial.Eval

open Cardinal in
lemma Polynomial.exists_eval_ne_zero_of_natDegree_lt_card {R : Type*} [CommRing R] [IsDomain R]
    (f : Polynomial R) (hf : f ≠ 0) (hfR : f.natDegree < #R) :
    ∃ r, f.eval r ≠ 0 := by
  sorry

[Johan Commelin]

I suppose the proof should use docs#Polynomial.card_roots

[Oliver Nash]

I don't have an answer to your question but you need coefficients to be a field, right? E.g., $2x + 1$ (with R = ℤ).

[Riccardo Brasca]

@Oliver Nash in the statement there is ≠ 0 (I am assuming you read something like ... = 0.

[Oliver Nash]

Thanks!

[Riccardo Brasca]

I think you can prove it quickly via docs#Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero

[Johan Commelin]

Thanks for the pointer!

[Riccardo Brasca]

Something along the lines of

import Mathlib

open Polynomial Cardinal Function in
lemma Polynomial.exists_eval_ne_zero_of_natDegree_lt_card {R : Type*} [CommRing R] [IsDomain R]
    (f : Polynomial R) (hf : f ≠ 0) (hfR : f.natDegree < #R) :
    ∃ r, f.eval r ≠ 0 := by
  by_contra! H
  by_cases hfin : Infinite R
  · exact hf <| zero_of_eval_zero _ H
  · have := fintypeOfNotInfinite hfin
    exact hf <| eq_zero_of_natDegree_lt_card_of_eval_eq_zero f injective_id H (by aesop)

[Riccardo Brasca]

Wasn't by_contra' renamed by_contra? I was expecting the get immediately the statement in the ∀ (x : R), eval x f = 0 form.

[Eric Rodriguez]

There's by_contra!

[Johan Commelin]

Thanks for the pointers

open Cardinal in
lemma Polynomial.exists_eval_ne_zero_of_natDegree_lt_card [IsDomain R]
    (f : Polynomial R) (hf : f ≠ 0) (hfR : f.natDegree < #R) :
    ∃ r, f.eval r ≠ 0 := by
  contrapose! hf
  obtain hR|hR := finite_or_infinite R
  · have := Fintype.ofFinite R
    apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero f Function.injective_id hf
    rw [mk_fintype] at hfR
    exact_mod_cast hfR
  · apply Polynomial.funext
    simpa using hf

[Riccardo Brasca]

If you want to use it, aesop can do the two lines about cardinality.

[Johan Commelin]

Nice