English
A technical equality expressing that evaluating a polynomial after applying a finite successor equivalence corresponds to evaluating with a transformed argument.
Русский
Техническое равенство, показывающее, что операция вычисления полинома после применения эквивалентности конечного продолжения соответствует вычислению с преобразованным аргументом.
LaTeX
$$$$ \\text{Polynomial.eval}(x, \\operatorname{finSuccEquiv}(R,n) f) = \\operatorname{Polynomial.eval}(\\cdot, f) \\text{ (формально записано).} $$$$
Lean4
theorem polynomial_eval_eval₂ [CommSemiring R] [CommSemiring S] {x : S} (f : R →+* Polynomial S) (g : σ → Polynomial S)
(p : MvPolynomial σ R) :
Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p :=
by
apply induction_on p
· simp
· intro p q hp hq
simp [hp, hq]
· intro p n hp
simp [hp]
