eval₂_pow' — Mathlib

English

For any polynomial p and natural n, (p^n) eval₂ with respect to f equals (p eval₂) raised to the nth power.

Русский

Для любой степень полинома p и натурального n выполняется (p^n) eval₂ = (p eval₂)^n.

LaTeX

$$$ (p^n).eval_2 (\\text{algebraMap } R S) x = (p. eval_2 (\\text{algebraMap } R S) x)^n$$$

Lean4

@[simp]
theorem eval₂_pow' (n : ℕ) : (p ^ n).eval₂ (algebraMap R S) x = (p.eval₂ (algebraMap R S) x) ^ n := by
  induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]

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