coeff_succ_mul_X — Mathlib

English

For n ∈ ℕ, φ ∈ R⟦X⟧, the coefficient of n+1 in φ·X equals the coefficient of n in φ.

Русский

Для n ∈ ℕ, φ ∈ R⟦X⟧, коэффициент степени n+1 в φ·X равен коэффициентy степени n в φ.

LaTeX

$$$\operatorname{coeff}_{n+1}(\varphi \cdot X) = \operatorname{coeff}_n(\varphi)$$$

Lean4

@[simp]
theorem coeff_succ_mul_X (n : ℕ) (φ : R⟦X⟧) : coeff (n + 1) (φ * X) = coeff n φ :=
  by
  simp only [coeff, Finsupp.single_add]
  convert φ.coeff_add_mul_monomial (single () n) (single () 1) _
  rw [mul_one]

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