coeff_reverse — Mathlib

English

For any f ∈ R[X], the nth coefficient of reverse f equals the coefficient of f at revAt(n, natDegree f): coeff(reverse f, n) = coeff(f, revAt(n, natDegree f)).

Русский

Для любого f ∈ R[X] коэффициент степени n в reverse f равен коэффициенту f на индексе revAt(n, natDegree f): coeff(reverse f, n) = coeff(f, revAt(n, natDegree f)).

LaTeX

$$$\operatorname{coeff}(\operatorname{reverse}(f), n) = \operatorname{coeff}\left(f, \operatorname{revAt}(\operatorname{natDegree}(f), n)\right).$$$

Lean4

theorem coeff_reverse (f : R[X]) (n : ℕ) : f.reverse.coeff n = f.coeff (revAt f.natDegree n) := by
  rw [reverse, coeff_reflect]

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