mirror_leadingCoeff — Mathlib

English

For any polynomial p, the leading coefficient of its mirror equals the trailing coefficient of p.

Русский

У зеркала полинома p ведущий коэффициент равен его последнему коэффициенту.

LaTeX

$$$ \\operatorname{leadingCoeff}(p^{\\sim}) = \\operatorname{trailingCoeff}(p) $$$

Lean4

@[simp]
theorem mirror_leadingCoeff : p.mirror.leadingCoeff = p.trailingCoeff := by
  rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]

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