English
For polynomials p, q over a ring, the root multiplicity after a certain shift and multiplication corresponds to the sum of root multiplicities, i.e., rootMultiplicity a (p · (X − C a)^n) = rootMultiplicity a p + n, under suitable non-zero conditions.
Русский
Для многочленов p, q над кольцом, кратность корня после сдвига и умножения равна сумме кратностей: rootMultiplicity a (p · (X − C a)^n) = rootMultiplicity a p + n при подходящих условиях.
LaTeX
$$$$ \\operatorname{rootMultiplicity} a \\big( p \\cdot (X - C a)^n \\big) = \\operatorname{rootMultiplicity} a(p) + n, \\text{ при } p \\neq 0. $$$$
Lean4
/-- The multiplicity of `a` as root of `(X - a) ^ n` is `n`. -/
theorem rootMultiplicity_X_sub_C_pow [Nontrivial R] (a : R) (n : ℕ) : rootMultiplicity a ((X - C a) ^ n) = n :=
by
have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero
rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
