fwdDiff_iter_finset_sum — Mathlib

English

For a ring R and a module G, the forward difference distributes over scalar multiplication by a fixed g: Δ_h (f • g) = (Δ_h f) • g.

Русский

Для кольца R и модуля G передняя разность распределяется по скалярному умножению на фиксированный элемент g: Δ_h (f • g) = (Δ_h f) • g.

LaTeX

$$$ \Delta_h (f \mapsto f \cdot g) = (\Delta_h f) \cdot g $$$

Lean4

@[simp]
theorem fwdDiff_iter_finset_sum {α : Type*} (s : Finset α) (f : α → M → G) (n : ℕ) :
    Δ_[h]^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, Δ_[h]^[n] (f k) := by
  simpa only [coe_fwdDiffₗ_pow] using map_sum (fwdDiffₗ M G h ^ n) f s

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