English
For a finite field R and a nonzero-degree polynomial p over R, the size of R is at most natDegree(p) times the size of the image of the evaluation map x ↦ p(x) as x runs through R.
Русский
Для конечного поля R и полинома p над R степенью больше нуля, |R| ≤ deg(p) · |{p(x) : x ∈ R}|.
LaTeX
$$$|R| \le \operatorname{natDegree}(p) \cdot \#\bigl(\operatorname{univ}.image(\lambda x, \operatorname{eval} x\, p)\bigr)$$$
Lean4
/-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
polynomial -/
theorem card_image_polynomial_eval [DecidableEq R] [Fintype R] {p : R[X]} (hp : 0 < p.degree) :
Fintype.card R ≤ natDegree p * #(univ.image fun x => eval x p) :=
Finset.card_le_mul_card_image _ _
(fun a _ =>
calc
_ = #(p - C a).roots.toFinset := congr_arg card (by simp [Finset.ext_iff, ← mem_roots_sub_C hp])
_ ≤ Multiset.card (p - C a).roots := (Multiset.toFinset_card_le _)
_ ≤ _ := card_roots_sub_C' hp)
