removeZero_of_pos — Mathlib

English

Let p be a formal multilinear series. If 0 < n, then removing zeros at index n leaves the coefficient unchanged: p.removeZero n = p n.

Русский

Пусть p — формальная мультилинейная серия. Если 0 < n, то удаление нулей на позиции n не меняет коэффициент: p.removeZero n = p n.

LaTeX

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

Lean4

theorem removeZero_of_pos (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (h : 0 < n) : p.removeZero n = p n :=
  by
  rw [← Nat.succ_pred_eq_of_pos h]
  rfl

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