Polynomial pigeonhole

Stream: Is there code for X?

[Violeta Hernández]

There's got to be some lemma that proves the brunt of this, but I'm not sure how to find it.

import Mathlib.Algebra.Polynomial.Degree.Defs
import Mathlib.Algebra.Polynomial.Eval.Defs
import Mathlib.Data.Set.Card

open Polynomial in
theorem ncard_polynomial_image {R : Type*} [Field R] (p : R[X]) (s : Set R) :
    s.ncard / p.natDegree ≤ (p.eval '' s).ncard := by
  sorry

The idea of course is that there can only be p.natDegree collisions per polynomial.

[Junyan Xu]

You should be able to show (p.eval ⁻¹' t).ncard ≤ p.natDegree * t.ncard from Polynomial.preimage_eval_singleton (recently added), then take t = p.eval '' s and use monotonicity of ncard. I wouldn't call this pigeonhole ...