neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq

English

The polynomial identity (-1)^n * shiftedLegendre(n) composed with (1 - X) equals shiftedLegendre(n).

Русский

Тождество: (-1)^n * shiftedLegendre(n) с композициями (1 - X) даёт shiftedLegendre(n).

LaTeX

$$$(-1)^n \\cdot \\mathrm{shiftedLegendre}(n) \\circ (1 - X) = \\mathrm{shiftedLegendre}(n)$$$

Lean4

theorem neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq (n : ℕ) :
    (-1) ^ n * (shiftedLegendre n).comp (1 - X) = shiftedLegendre n :=
  by
  refine nat_mul_inj' ?_ (factorial_ne_zero n)
  rw [← mul_assoc, mul_comm (n ! : ℤ[X]), mul_assoc, ← natCast_mul_comp, factorial_mul_shiftedLegendre_eq, ←
    iterate_derivative_comp_one_sub_X]
  simp [mul_comm]

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