English
For polynomials p, q ∈ R[X] and x ∈ R, if p q ≠ 0, then rootMultiplicity x (p q) = rootMultiplicity x p + rootMultiplicity x q.
Русский
Для многочленов p, q ∈ R[X] и элемента x ∈ R, если p q ≠ 0, то сумма кратностей корня равна сумме кратностей корней.
LaTeX
$$rootMultiplicity x (p q) = rootMultiplicity x p + rootMultiplicity x q, \quad \text{whenever } p q \neq 0.$$
Lean4
theorem rootMultiplicity_mul {p q : R[X]} {x : R} (hpq : p * q ≠ 0) :
rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q := by
classical
have hp : p ≠ 0 := left_ne_zero_of_mul hpq
have hq : q ≠ 0 := right_ne_zero_of_mul hpq
rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p, if_neg hp,
rootMultiplicity_eq_multiplicity q, if_neg hq,
multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
