le_rootMultiplicity_mul — Mathlib

English

For polynomials p, q, x ∈ R with p q ≠ 0, rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p q).

Русский

Для полиномов p, q и элемента x с p q ≠ 0 имеем: кратность x к p и к q суммарно не превосходит кратность x к p q.

LaTeX

$$$ \operatorname{rootMultiplicity}(x,p) + \operatorname{rootMultiplicity}(x,q) \le \operatorname{rootMultiplicity}(x, p q) $ при $ p q \neq 0 $.$$

Lean4

theorem le_rootMultiplicity_mul {p q : R[X]} (x : R) (hpq : p * q ≠ 0) :
    rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q) :=
  by
  rw [le_rootMultiplicity_iff hpq, pow_add]
  gcongr <;> apply pow_rootMultiplicity_dvd

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