expand_eval

Mathlib.Algebra.Polynomial.Expand

URI: https://scilib.ai/kg/mathlib#Polynomial.expand_eval

← MathLib Explorer

English

If p > 0, then (expand p f).coeff (n p) = f.coeff n.

Русский

Если p>0, то (expand p f).coeff (n p) = f.coeff n.

LaTeX

$$$(\operatorname{expand}(R,p) f).\mathrm{coeff}(n p) = f.\mathrm{coeff}(n)$$$

Lean4

@[simp]
theorem expand_eval (p : ℕ) (P : R[X]) (r : R) : eval r (expand R p P) = eval (r ^ p) P :=
  by
  refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
  rw [map_add, eval_add, eval_add, hf, hg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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