eval₂_rename — Mathlib

English

For k: σ → τ, f: R →+* S, and p ∈ MvPolynomial σ R, the two-variable evaluation commutes with rename: (rename k p).eval₂ f g = p.eval₂ f (g ∘ k).

Русский

Для k: σ → τ, гомоморфизма f: R →+* S и p ∈ MvPolynomial σ R, двойная оценка коммутирует с переименованием: (rename k p).eval₂ f g = p.eval₂ f (g ∘ k).

LaTeX

$$$\\bigl(\\text{rename } k\\, p\\bigr)\\_{{eval_2}} f g = p\\_{{eval_2}} f (g \\circ k).$$$

Lean4

theorem eval₂_rename : (rename k p).eval₂ f g = p.eval₂ f (g ∘ k) := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

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