fwdDiff_iter_const_smul — Mathlib

English

For r ∈ R and f: M → G, the nth forward difference commutes with constant smul: Δ_h^[n] (r • f) = r • Δ_h^[n] f.

Русский

Для r ∈ R и f: M → G н-я передняя разность коммутирует умножение на константу: Δ_h^[n] (r • f) = r • Δ_h^[n] f.

LaTeX

$$$ \Delta_h^{[n]} (r \cdot f) = r \cdot \Delta_h^{[n]} f $$$

Lean4

@[simp]
theorem fwdDiff_iter_const_smul {R : Type*} [Monoid R] [DistribMulAction R G] (r : R) (f : M → G) (n : ℕ) :
    Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f := by
  induction n generalizing f with
  | zero => simp only [iterate_zero, id_eq]
  | succ n IH => simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

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