count_roots_le_one — Mathlib

English

If p is separable over a field, then the number of distinct roots of p in F is at most 1 for each value, i.e., p has at most one root equal to a given element.

Русский

Если p сепарабелен над полем, то число различных корней p в F для каждого значения не превышает 1.

LaTeX

$$$ p \text{ Separable } \Rightarrow \forall x \in F, \#\{\alpha : F \mid p(\alpha)=0 \} \le 1$$$

Lean4

theorem count_roots_le_one [DecidableEq R] {p : R[X]} (hsep : Separable p) (x : R) : p.roots.count x ≤ 1 :=
  by
  rw [count_roots p]
  exact rootMultiplicity_le_one_of_separable hsep x

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