toLaurent_reverse — Mathlib

English

For any polynomial p ∈ R[X], the Laurent image of its reversal satisfies a simple relation: toLaurent(p.reverse) = invert(toLaurent(p)) · T^{natDegree(p)}.

Русский

Для любого полинома p ∈ R[X] лорантовое изображение его разворота удовлетворяет простой зависимости: toLaurent(p.reverse) = invert(toLaurent(p)) · T^{natDegree(p)}.

LaTeX

$$$ \mathrm{toLaurent}(p^{\text{reverse}}) = \operatorname{invert}( \mathrm{toLaurent}(p) ) \cdot T^{\mathrm{natDegree}(p)} $$$

Lean4

theorem toLaurent_reverse (p : R[X]) : toLaurent p.reverse = invert (toLaurent p) * (T p.natDegree) :=
  by
  nontriviality R
  induction p using Polynomial.recOnHorner with
  | M0 => simp
  | MC _ _ _ _ ih => simp [add_mul, ← ih]
  | MX _ hp => simpa [natDegree_mul_X hp]

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