rootMultiplicity_eq_zero_iff — Mathlib

English

The statement rootMultiplicity x p = 0 is equivalent to: if IsRoot p x holds then p = 0.

Русский

Утверждение: rootMultiplicity x p = 0 эквивалентно тому, что если p имеет x как корень, то p = 0.

LaTeX

$$$ \operatorname{rootMultiplicity}(x,p) = 0 \iff (\operatorname{IsRoot}(p,x) \to p = 0) $$$

Lean4

@[simp]
theorem rootMultiplicity_eq_zero_iff {p : R[X]} {x : R} : rootMultiplicity x p = 0 ↔ IsRoot p x → p = 0 := by
  classical
    simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff, multiplicity_eq_zero, dvd_iff_isRoot, not_imp_not]

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