fwdDiff_smul_const — Mathlib

English

Let R be a Ring and G an R-module. For a function f: M → R and a fixed g ∈ G, the forward difference of the function y ↦ f(y) · g is equal to the function y ↦ (Δ_h f)(y) · g.

Русский

Пусть R — кольцо, G — модуль над R. Для функции f: M → R и фиксированного g ∈ G передняя разность функции y ↦ f(y) · g равна функции y ↦ (Δ_h f)(y) · g.

LaTeX

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

Lean4

@[simp]
theorem fwdDiff_smul_const {R : Type} [Ring R] [Module R G] (f : M → R) (g : G) :
    Δ_[h] (fun y ↦ f y • g) = Δ_[h] f • fun _ ↦ g := by
  ext y
  simp only [fwdDiff, Pi.smul_apply', sub_smul]

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