eval_rename_prod_mk — Mathlib

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 _) _ _ _

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