English
If f₁ and f₂ are ring homomorphisms and p₁, p₂ are polynomials with the same behavior on constants and on the variables they contain, then f₁ p₁ = f₂ p₂ whenever p₁ = p₂.
Русский
Если f₁ и f₂ — кольцевые гомоморфизмы и полиномы p₁, p₂ совпадают на константах и на переменных, которые они содержат, то f₁ p₁ = f₂ p₂ при p₁ = p₂.
LaTeX
$$$ f_1 p_1 = f_2 p_2 $ при условиях согласованности$$
Lean4
/-- If `f₁` and `f₂` are ring homs out of the polynomial ring and `p₁` and `p₂` are polynomials,
then `f₁ p₁ = f₂ p₂` if `p₁ = p₂` and `f₁` and `f₂` are equal on `R` and on the variables
of `p₁`. -/
theorem hom_congr_vars {f₁ f₂ : MvPolynomial σ R →+* S} {p₁ p₂ : MvPolynomial σ R} (hC : f₁.comp C = f₂.comp C)
(hv : ∀ i, i ∈ p₁.vars → i ∈ p₂.vars → f₁ (X i) = f₂ (X i)) (hp : p₁ = p₂) : f₁ p₁ = f₂ p₂ :=
calc
f₁ p₁ = eval₂Hom (f₁.comp C) (f₁ ∘ X) p₁ := RingHom.congr_fun (by ext <;> simp) _
_ = eval₂Hom (f₂.comp C) (f₂ ∘ X) p₂ := (eval₂Hom_congr' hC hv hp)
_ = f₂ p₂ := RingHom.congr_fun (by ext <;> simp) _
