mirror — Mathlib

English

The mirror of a polynomial reverses its coefficients and shifts by the natTrailingDegree to preserve natDegree.

Русский

Зеркало полинома обращает коэффициенты и сдвигает на natTrailingDegree, чтобы сохранить natDegree.

LaTeX

$$$ \operatorname{mirror}(p) = \operatorname{reverse}(p) \cdot X^{\operatorname{natTrailingDegree}(p)} $$$

Lean4

/-- mirror of a polynomial: reverses the coefficients while preserving `Polynomial.natDegree` -/
noncomputable def mirror :=
  p.reverse * X ^ p.natTrailingDegree

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