English
If q is monic and x is a root of q in an algebra, then evaluating p modulo q at x equals evaluating p at x.
Русский
Если q монический и x является корнем q в алгебре, то aeval x (p mod q) = aeval x p.
LaTeX
$$$$ \\operatorname{aeval}_x (p \\bmod_{\\! m} q) = \\operatorname{aeval}_x p, \\quad q.Monic, \\ hx : \\operatorname{aeval}_x q = 0. $$$$
Lean4
theorem rootMultiplicity_mul_X_sub_C_pow {p : R[X]} {a : R} {n : ℕ} (h : p ≠ 0) :
(p * (X - C a) ^ n).rootMultiplicity a = p.rootMultiplicity a + n :=
by
have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
refine le_antisymm ?_ ?_
· rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
exact pow_rootMultiplicity_not_dvd h a
· rw [le_rootMultiplicity_iff h2, pow_add]
exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _
