fwdDiff_addChar_eq — Mathlib

English

For AddChar φ, the nth forward difference satisfies Δ_h^[n] φ x = (φ(h) - 1)^n · φ(x).

Русский

Для AddChar φ имеет место Δ_h^[n] φ x = (φ(h) - 1)^n · φ(x).

LaTeX

$$$ Δ_h^{[n]} \varphi x = (\varphi(h) - 1)^n \cdot \varphi x $$$

Lean4

theorem fwdDiff_addChar_eq {M R : Type*} [AddCommMonoid M] [Ring R] (φ : AddChar M R) (x h : M) (n : ℕ) :
    Δ_[h]^[n] φ x = (φ h - 1) ^ n * φ x := by
  induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]
    rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]

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