English
Under a nonvanishing condition, the root multiplicity of a product p q at x equals the sum of the root multiplicities at x of p and q.
Русский
При условии ненулевой величины произведения кратности корня x складываются: rootMultiplicity x (p q) = rootMultiplicity x p + rootMultiplicity x q.
LaTeX
$$$$ \\text{If } (p /ₘ (X - C x) ^ p.rootMultiplicity x) .eval x \\cdot (q /ₘ (X - C x) ^ q.rootMultiplicity x).eval x \\neq 0 \\;\\Rightarrow\\; \\operatorname{rootMultiplicity} x (p q) = \\operatorname{rootMultiplicity} x p + \\operatorname{rootMultiplicity} x q. $$$$
Lean4
theorem rootMultiplicity_mul' {p q : R[X]} {x : R}
(hpq : (p /ₘ (X - C x) ^ p.rootMultiplicity x).eval x * (q /ₘ (X - C x) ^ q.rootMultiplicity x).eval x ≠ 0) :
rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q :=
by
simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq
simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]
