English
The evaluation at t of p divided by (X - C t)^{rootMultiplicity t p} equals the trailing coefficient of p composed with (X + C t).
Русский
Значение в t полинома p, поделенного на (X − C t)^{rootMultiplicity t p}, равно последнему коэффициенту состава p ◦ (X + C t).
LaTeX
$$$ \operatorname{eval}_t\left(p /_{\mathrm{monic}} (X - C t)^{\operatorname{rootMultiplicity}(t,p)}\right) = \operatorname{trailingCoeff}\left(p\circ (X + C t)\right) $$$
Lean4
theorem eval_divByMonic_eq_trailingCoeff_comp {p : R[X]} {t : R} :
(p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t = (p.comp (X + C t)).trailingCoeff :=
by
obtain rfl | hp := eq_or_ne p 0
· rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t
set m := p.rootMultiplicity t
set g := p /ₘ (X - C t) ^ m
have : (g.comp (X + C t)).coeff 0 = g.eval t := by
rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp, add_sub_cancel_right, ←
reverse_leadingCoeff, reverse_X_pow_mul, reverse_leadingCoeff, trailingCoeff,
Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <| this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp), this]
