removeZero_coeff_succ — Mathlib

English

Let p be a formal multilinear series. For every natural number n > 0, the coefficient obtained after discarding the zeroth term satisfies p.removeZero n = p n.

Русский

Пусть p — форма многочленов с переменными. Для каждого натурального n > 0 коэффициент после удаления нулевого члена удовлетворяет p.removeZero n = p n.

LaTeX

$$$0 < n \Rightarrow p.removeZero\,n = p\,n$$$

Lean4

@[simp]
theorem removeZero_coeff_succ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : p.removeZero (n + 1) = p (n + 1) :=
  rfl

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