reverse_trailingCoeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem reverse_trailingCoeff (f : R[X]) : f.reverse.trailingCoeff = f.leadingCoeff := by
  rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]

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