coeff_iterate_fslope — Mathlib

English

For k ∈ ℕ and n ∈ ℕ, the nth coefficient of the k-fold iterate of fslope applied to p equals p.coeff (n + k): (fslope^[k] p).coeff n = p.coeff (n + k).

Русский

При k раз применения fslope к p, n-й коэффициент равен коэффициенту p при n + k: (fslope^[k] p).coeff n = p.coeff (n + k).

LaTeX

$$$ (fslope^{[k]} p).coeff n = p.coeff (n + k) $$$

Lean4

@[simp]
theorem coeff_iterate_fslope (k n : ℕ) : (fslope^[k] p).coeff n = p.coeff (n + k) := by
  induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]

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