expand_aeval — Mathlib

English

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

Русский

Для p>0, (expand p f).coeff (p n) = f.coeff n.

LaTeX

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

Lean4

@[simp]
theorem expand_aeval {A : Type*} [Semiring A] [Algebra R A] (p : ℕ) (P : R[X]) (r : A) :
    aeval r (expand R p P) = aeval (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, aeval_add, aeval_add, hf, hg]

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