English
If g : σ × τ → R and i ∈ σ, then evaluating after renaming by Prod.mk i is the same as evaluating with the projected function, i.e. eval g (rename (Prod.mk i) p) = eval (λ j, g (i, j)) p.
Русский
Пусть g : σ × τ → R и i ∈ σ. Тогда eval g после переименования по Prod.mk i равен eval с проекцией: eval g (rename (Prod.mk i) p) = eval (λ j, g (i, j)) p.
LaTeX
$$$ \mathrm{eval}\ g\ (\mathrm{rename} (\mathrm{Prod.mk}\ i)\ p) = \mathrm{eval}\ (\lambda j. g (i, j))\ p $$$
Lean4
theorem eval_rename_prod_mk (g : σ × τ → R) (i : σ) (p : MvPolynomial τ R) :
eval g (rename (Prod.mk i) p) = eval (fun j => g (i, j)) p :=
eval₂_rename_prod_mk (RingHom.id _) _ _ _