reflect_C_mul_X_pow — Mathlib

English

Reflect sends constant times X^n to the constant times X^{revAt N n}.

Русский

Reflect отправляет константу, умноженную на X^n, в константу, умноженную на X^{revAt N n}.

LaTeX

$$$\\mathrm{reflect}\\ N\\ (C\\ c\\cdot X^n) = C\\ c\\cdot X^{\\mathrm{revAt}\\ N\\ n}.$$$

Lean4

theorem reflect_C_mul_X_pow (N n : ℕ) {c : R} : reflect N (C c * X ^ n) = C c * X ^ revAt N n :=
  by
  ext
  rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]
  split_ifs with h
  · rw [h, revAt_invol, coeff_X_pow_self]
  · rw [notMem_support_iff.mp]
    intro a
    rw [← one_mul (X ^ n), ← C_1] at a
    apply h
    rw [← mem_support_C_mul_X_pow a, revAt_invol]

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