zero_of_eval_zero — Mathlib

English

If a polynomial p ∈ R[X] vanishes at every element of an infinite ring R, then p is the zero polynomial

Русский

Если полином p ∈ R[X] обращается в нуль для всех элементов бесконечного кольца R, то p = 0.

LaTeX

$$[Infinite R] ∧ p ∈ R[X] ∧ (∀ x ∈ R, p.eval x = 0) ⇒ p = 0$$

Lean4

theorem zero_of_eval_zero [Infinite R] (p : R[X]) (h : ∀ x, p.eval x = 0) : p = 0 := by
  classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

Похожие утверждения