English
If f₁ and f₂ are ring homomorphisms and p₁ and p₂ are polynomials with matching behavior on constants and variables, then eval₂Hom f₁ g₁ p₁ = eval₂Hom f₂ g₂ p₂ when p₁ = p₂.
Русский
Если f₁ и f₂ — кольцевые гомоморфизмы, и p₁, p₂ — полиномы, удовлетворяющие совместимым условиям на константы и переменные, то равенство выполняется при p₁ = p₂.
LaTeX
$$$ eval₂Hom f_1 g_1 p_1 = eval₂Hom f_2 g_2 p_2 $$$
Lean4
theorem eval₂Hom_congr' {f₁ f₂ : R →+* S} {g₁ g₂ : σ → S} {p₁ p₂ : MvPolynomial σ R} :
f₁ = f₂ → (∀ i, i ∈ p₁.vars → i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → eval₂Hom f₁ g₁ p₁ = eval₂Hom f₂ g₂ p₂ :=
by
rintro rfl h rfl
rw [p₁.as_sum]
simp only [map_sum, eval₂Hom_monomial]
apply Finset.sum_congr rfl
intro d hd
congr 1
simp only [Finsupp.prod]
apply Finset.prod_congr rfl
intro i hi
have : i ∈ p₁.vars := by
rw [mem_vars]
exact ⟨d, hd, hi⟩
rw [h i this this]
