eq_zero_of_infinite_isRoot — Mathlib

English

Let R be a domain and p ∈ R[X]. If the set { x ∈ R | IsRoot p x } is infinite, then p = 0.

Русский

Пусть R — область целых чисел (домейн) и p ∈ R[X]. Если множество x ∈ R such that p.IsRoot x бесконечно, то p = 0.

LaTeX

$$$ (p \in R[X]) \wedge \operatorname{Set.Infinite}\{ x \in R \mid IsRoot(p,x)\} \Rightarrow p = 0 $$$

Lean4

theorem eq_zero_of_infinite_isRoot (p : R[X]) (h : Set.Infinite {x | IsRoot p x}) : p = 0 :=
  not_imp_comm.mp finite_setOf_isRoot h

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