reverse — Mathlib

English

The reverse of a polynomial f is defined as reverse f = reflect (natDegree f) f; equivalently, reverse f = f(1/X) · X^{natDegree f}.

Русский

Обратный многочлен f определяется как reverse f = reflect (natDegree f) f; эквивалентно reverse f = f(1/X) · X^{natDegree f}.

LaTeX

$$$\operatorname{reverse}(f) = \operatorname{reflect}(\operatorname{natDegree}(f))\,f.$$$

Lean4

/-- The reverse of a polynomial f is the polynomial obtained by "reading f backwards".
Even though this is not the actual definition, `reverse f = f (1/X) * X ^ f.natDegree`. -/
noncomputable def reverse (f : R[X]) : R[X] :=
  reflect f.natDegree f

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