eval₂_rename_prod_mk — Mathlib

English

For any i ∈ σ and p ∈ MvPolynomial τ R and any function g : σ × τ → S, (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p.

Русский

Для любого i ∈ σ и p ∈ MvPolynomial τ R и любой g : σ × τ → S выполняется: (rename (Prod.mk i) p).eval₂ f g = eval₂ f (λ j, g (i, j)) p.

LaTeX

$$$ (\mathrm{rename} (\mathrm{Prod.mk}\ i)\ p)\,\mathrm{eval}_2\ f\ g = p\,\mathrm{eval}_2\ f\ (\lambda j. g (i, j)) $$$

Lean4

theorem eval₂_rename_prod_mk (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) :
    (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

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