coeff_one_reverse — Mathlib

English

The coefficient of reverse f at 1 equals nextCoeff f: coeff(reverse f, 1) = nextCoeff f.

Русский

Коэффициент обратного при степени 1 равен nextCoeff f: coeff(reverse f, 1) = nextCoeff f.

LaTeX

$$$\operatorname{coeff}(\operatorname{reverse}(f), 1) = \operatorname{nextCoeff}(f).$$$

Lean4

@[simp]
theorem coeff_one_reverse (f : R[X]) : coeff (reverse f) 1 = nextCoeff f :=
  by
  rw [coeff_reverse, nextCoeff]
  split_ifs with hf
  · have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
    simp [*, revAt]
  · rw [revAt_le]
    exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

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