mirror_trailingCoeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mirror_trailingCoeff : p.mirror.trailingCoeff = p.leadingCoeff := by
  rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror, revAt_le (Nat.le_add_left _ _),
    add_tsub_cancel_right]

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