English
For RingHom f, polynomials p, q and natural k, eval₂ f t (Nat.iterate p.comp k q) equals Nat.iterate (λx, eval₂ f x p) k (eval₂ f t q).
Русский
Для кольцевого гомоморфа f, полиномов p, q и натурального k выполняется eval₂ f t (Nat.iterate p.comp k q) = Nat.iterate (λx, eval₂ f x p) k (eval₂ f t q).
LaTeX
$$$\\operatorname{eval}_2 f t \\big(\\mathrm{Nat.iterate}(p\\;\\mathrm{comp}\\;k\\;q)\\big) = \\mathrm{Nat.iterate}\\big(\\lambda x. \\operatorname{eval}_2 f x p\\big)\\ k\\big(\\operatorname{eval}_2 f t q\\big)$$$
Lean4
@[simp]
theorem iterate_comp_eval₂ (k : ℕ) (t : S) : eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q) := by
induction k with
| zero => simp
| succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
