coeff_zero_reverse — Mathlib

English

The 0-th coefficient of reverse f equals the leading coefficient of f: coeff(reverse f, 0) = leadingCoeff(f).

Русский

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

LaTeX

$$$\operatorname{coeff}(\operatorname{reverse}(f), 0) = \operatorname{leadingCoeff}(f).$$$

Lean4

@[simp]
theorem coeff_zero_reverse (f : R[X]) : coeff (reverse f) 0 = leadingCoeff f := by
  rw [coeff_reverse, revAt_le (zero_le f.natDegree), tsub_zero, leadingCoeff]

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