fwdDiff_const_smul — Mathlib

English

Let h ∈ M and (R, G) with a module structure. For r ∈ R and f: M → G, the nth forward difference of r · f equals r · the nth forward difference of f: Δ_h (r · f) = r · Δ_h f.

Русский

Пусть h ∈ M и дано структура модуля. Для r ∈ R и f: M → G верно Δ_h (r · f) = r · Δ_h f.

LaTeX

$$$ \Delta_h (r \cdot f) = r \cdot \Delta_h f $$$

Lean4

@[simp]
theorem fwdDiff_const_smul {R : Type*} [Monoid R] [DistribMulAction R G] (r : R) (f : M → G) :
    Δ_[h] (r • f) = r • Δ_[h] f :=
  funext fun _ ↦ (smul_sub ..).symm

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