Theorems · Definition · difference equations

fwdDiff

{M : Type u_1} → {G : Type u_2} → [AddCommMonoid M] → [AddCommGroup G] → M → (M → G) → M → G

Forward difference operator, fwdDiff h f n = f (n + h) - f n. The notation Δ_[h] for this operator is available in the fwdDiff namespace.

Defined in

Mathlib.Algebra.Group.ForwardDiff

Cited by

35 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddCommMonoidAddCommGroup