eval₂_pow

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_pow

English

Evaluating a power of a polynomial commutes with taking powers: eval₂(f,x)(p^n) = (eval₂(f,x)p)^n.

Русский

Оценка степени полинома расходится с возведением в степень: eval₂(f,x)(p^n) = (eval₂(f,x)p)^n.

LaTeX

$$$(p^n).\operatorname{eval}_{2} f x = (p.\operatorname{eval}_{2} f x)^n$$$

Lean4

theorem eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n :=
  (eval₂RingHom _ _).map_pow _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru