coeff_succ_X_mul — 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}(X \cdot \varphi) = \operatorname{coeff}_n(\varphi)$$$

Lean4

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

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