English
Let R be a ring, G an R-module, f: M → R and g: M → G. Then the forward difference of the product f · g is given by Δ_h (f · g) = (Δ_h f) · g + f · (Δ_h g) + (Δ_h f) · (Δ_h g).
Русский
Пусть R — кольцо, G — модуль над R, f: M → R и g: M → G. Тогда передняя разность произведения f · g равна Δ_h (f) · g + f · Δ_h (g) + Δ_h (f) · Δ_h (g).
LaTeX
$$$ \Delta_h (f g) = (\Delta_h f) \cdot g + f \cdot (\Delta_h g) + (\Delta_h f) \cdot (\Delta_h g) $$$
Lean4
theorem fwdDiff_smul {R : Type} [Ring R] [Module R G] (f : M → R) (g : M → G) :
Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g :=
by
ext y
simp only [fwdDiff, Pi.smul_apply', Pi.add_apply, smul_sub, sub_smul]
abel
-- Note `fwdDiff_const_smul` is more general than `fwdDiff_smul` since it allows `R` to be a
-- semiring, rather than a ring; in particular `R = ℕ` is allowed.
