neg_one_pow_natDegree_mul_comp_neg_X

English

If p is monic, then the polynomial (-1)^{natDegree(p)} · p(comp(-X)) is monic.

Русский

Если p моничен, то (-1)^{natDegree(p)} · p(comp(-X)) является моническим.

LaTeX

$$$$ ((-1)^{\\operatorname{natDegree} p} \\cdot p( -X )).\\mathrm{Monic} = 1. $$$$

Lean4

theorem neg_one_pow_natDegree_mul_comp_neg_X {p : R[X]} (hp : p.Monic) : ((-1) ^ p.natDegree * p.comp (-X)).Monic :=
  by
  simp only [Monic]
  calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

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