English
If q is non-constant (deg q ≠ 0), the leading coefficient of the composition p ∘ q equals the product of the leading coefficient of p and the leading coefficient of q raised to the power deg p.
Русский
Если deg q ≠ 0, то ведущий коэффициент композиции p ∘ q равен произведению ведущего коэффициента p и возведённого в степень deg p ведущего коэффициента q.
LaTeX
$$$\\operatorname{natDegree}(q) \\neq 0 \\Rightarrow \\operatorname{leadingCoeff}(p\\circ q) = \\operatorname{leadingCoeff}(p) \\cdot (\\operatorname{leadingCoeff}(q))^{\\operatorname{natDegree}(p)}$$$
Lean4
theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p := by
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
