changeOriginSeriesTerm_bound — Mathlib

English

If p_m = 0 for all m with n ≤ m, then for all m with n ≤ k + m, p.changeOriginSeries k m = 0.

Русский

Если все коэффициенты после степени n нулевые, то для всех m с n ≤ k+m p.changeOriginSeries k m = 0.

LaTeX

$$∀ m, n ≤ k+m → p.changeOriginSeries k m = 0$$

Lean4

/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOriginSeriesTerm k l = 0` for `n ≤ k + l`. -/
theorem changeOriginSeriesTerm_bound (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0)
    (k l : ℕ) {s : Finset (Fin (k + l))} (hs : s.card = l) (hkl : n ≤ k + l) : p.changeOriginSeriesTerm k l s hs = 0 :=
  by rw [changeOriginSeriesTerm, hn _ hkl, map_zero]

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