iterate_comp_eval — Mathlib

English

For RingHom f and polynomials p, q, and natural k, eval t (Nat.iterate p.comp k q) equals Nat.iterate (λx, eval x p) k (eval t q).

Русский

Для кольцевого гомоморфа f и полиномов p, q и натурального k выполняется eval t (Nat.iterate p.comp k q) = Nat.iterate (λx, eval x p) k (eval t q).

LaTeX

$$$\\operatorname{eval} \\ t (\\mathrm{Nat.iterate}(p\\circ k\\;q)) = \\mathrm{Nat.iterate}\\big(\\lambda x. \\operatorname{eval} x p\\big)\\ k\\big(\\operatorname{eval} t q\\big)$$$

Lean4

@[simp]
theorem iterate_comp_eval : ∀ (k : ℕ) (t : R), (p.comp^[k] q).eval t = (fun x => p.eval x)^[k] (q.eval t) :=
  iterate_comp_eval₂ _

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