English
Let j ∈ τ and g : σ → MvPolynomial σ R. Then renaming p by Prod.mk j distributes over eval₂ with C, i.e., rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C (fun x => rename (Prod.mk j) (g x)).
Русский
Пусть j ∈ τ и задано g : σ → MvPolynomial σ R. Тогда переименование p по Prod.mk j распространяется на eval₂ с C: rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C (fun x => rename (Prod.mk j) (g x)).
LaTeX
$$$ \mathrm{rename} (\mathrm{Prod.mk}\ j)\bigl(p\,\mathrm{eval}_2\ C\ g\bigr) = p\,\mathrm{eval}_2\ C\ (\lambda x. \mathrm{rename} (\mathrm{Prod.mk}\ j)\ (g\ x)) $$$
Lean4
theorem rename_prod_mk_eval₂ (j : τ) (g : σ → MvPolynomial σ R) :
rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C fun x => rename (Prod.mk j) (g x) := by
apply MvPolynomial.induction_on p <;>
· intros
simp [*]
