coe_fwdDiffₗ_pow — Mathlib

English

The nth power of the forward-difference linear map equals the nth iterate of the forward-difference operator: the nth power of fwdDiff_ℓ equals fwdDiff^[n].

Русский

Пусть fwdDiff_ℓ — линейное отображение, тогда его n-я степенная композиция совпадает с n-й итерацией операторa передней разности: (fwdDiff_ℓ)^n = fwdDiff^[n].

LaTeX

$$$ ↑\bigl(fwdDiff_\ell M G h^n\bigr) = (fwdDiff h)^{[n]} $$$

Lean4

theorem coe_fwdDiffₗ_pow (n : ℕ) : ↑(fwdDiffₗ M G h ^ n) = (fwdDiff h)^[n] := by ext;
  rw [Module.End.pow_apply, coe_fwdDiffₗ]

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