English
For any polynomials p in MvPolynomial σ R, and any function g: τ → MvPolynomial σ R, the operation of renaming by k commutes with evaluating p using the map g, i.e., rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g).
Русский
Для любого p ∈ MvPolynomial σ R и любой g: τ → MvPolynomial σ R выполняется: rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g).
LaTeX
$$$ \text{rename } k\,(p\,\mathrm{eval}_2\ C\ (g \circ k)) = (\text{rename } k\ p)\,\mathrm{eval}_2\ C\ (\text{rename } k \circ g) $$$
Lean4
theorem rename_eval₂ (g : τ → MvPolynomial σ R) : rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g) :=
by
apply MvPolynomial.induction_on p <;>
· intros
simp [*]
