reverse_leadingCoeff — Mathlib

English

The leading coefficient of the reverse equals the trailing coefficient of the original: leadingCoeff(reverse f) = trailingCoeff(f).

Русский

Ведущий коэффициент обратного многочлена равен хвостовому коэффициенту исходного: leadingCoeff(reverse f) = trailingCoeff(f).

LaTeX

$$$\operatorname{leadingCoeff}(\operatorname{reverse}(f)) = \operatorname{trailingCoeff}(f).$$$

Lean4

theorem reverse_leadingCoeff (f : R[X]) : f.reverse.leadingCoeff = f.trailingCoeff := by
  rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree, coeff_reverse, revAt_invol,
    trailingCoeff]

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