English
For any a ∈ R and nonzero p, the factor X − C a has finite multiplicity in p.
Русский
Для любого a ∈ R и ненулевого p полином X − C a встречается с конечной кратностью в p.
LaTeX
$$$$ \\text{FiniteMultiplicity}(X - C a)\\, p. $$$$
Lean4
@[simp]
theorem modByMonic_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a) :=
by
nontriviality R
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul,
sub_zero]
have : degree (p %ₘ (X - C a)) < 1 := degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
have : degree (p %ₘ (X - C a)) ≤ 0 := by
revert this
cases degree (p %ₘ (X - C a))
· exact fun _ => bot_le
· exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))
rw [eq_C_of_degree_le_zero this, eval_C] at h
rw [eq_C_of_degree_le_zero this, h]
