rootMultiplicity_add — Mathlib

English

If p ≠ 0, then 0 < rootMultiplicity x p ↔ IsRoot p x.

Русский

Если p ≠ 0, то 0 < rootMultiplicity x p ↔ IsRoot p x.

LaTeX

$$$ (p \neq 0) \Rightarrow (0 < \operatorname{rootMultiplicity}(x,p) \iff IsRoot(p,x)) $$$

Lean4

/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
theorem rootMultiplicity_add {p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
    min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q) :=
  by
  rw [le_rootMultiplicity_iff hzero]
  exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

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