comp_neg_X_leadingCoeff_eq — Mathlib

English

Over a ring, the leading coefficient of p(−X) equals (−1)^{deg p} times the leading coefficient of p.

Русский

Пусть R — кольцо. Ведущий коэффициент p(−X) равен (−1)^{deg p} умноженному на ведущий коэффициент p.

LaTeX

$$$\\operatorname{leadingCoeff}(p\\circ(-X)) = (-1)^{\\operatorname{natDegree}(p)} \\operatorname{leadingCoeff}(p)$$$

Lean4

@[simp]
theorem comp_neg_X_leadingCoeff_eq [Ring R] (p : R[X]) :
    (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff :=
  by
  nontriviality R
  by_cases h : p = 0
  · simp [h]
  rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree] <;>
    simp [((Commute.neg_one_left _).pow_left _).eq, h]

Похожие утверждения