English
Let R be a domain and p ∈ R[X], a ∈ R with deg p ≠ 0. Then the leading coefficient of the quotient of p by the monic X − C a equals the leading coefficient of p.
Русский
Пусть R — область, p ∈ R[X], a ∈ R и deg p ≠ 0. Тогда ведущий коэффициент частного p на моническое X − C a равен ведущему коэффициенту p.
LaTeX
$$$\deg(p) \neq 0 \Rightarrow \operatorname{leadingCoeff}\left(\dfrac{p}{_{\mathrm{monic}}(X - C a)}\right) = \operatorname{leadingCoeff}(p).$$$
Lean4
theorem leadingCoeff_divByMonic_X_sub_C (p : R[X]) (hp : degree p ≠ 0) (a : R) :
leadingCoeff (p /ₘ (X - C a)) = leadingCoeff p :=
by
nontriviality
rcases hp.lt_or_gt with hd | hd
· rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]
refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]
