rootMultiplicity_le_one_of_separable

English

If p ∈ R[X] is separable, then for every x ∈ R, the multiplicity of x as a root of p is at most 1.

Русский

Если p ∈ R[X] сепарабелен, то для каждого x ∈ R кратность x как корня p не превосходит 1.

LaTeX

$$$ \\forall x \\in R,\\,\; \\operatorname{rootMultiplicity}(x,p) \\le 1$$$

Lean4

theorem rootMultiplicity_le_one_of_separable [Nontrivial R] {p : R[X]} (hsep : Separable p) (x : R) :
    rootMultiplicity x p ≤ 1 := by
  classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞), Nat.cast_one, ←
    (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep

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