English
The push-forward of a polynomial ring under a ring homomorphism aligns with evaluation at the images of the base constants and variables; more precisely, for a RingHom ϕ, map ϕ equals eval₂ with ϕ ∘ C and ϕ(X_s).
Русский
Перемещение кольцевого гомоморфа порождает эквивалентность между отображением и оценкой через изображения констант и переменных.
LaTeX
$$$\forall \{R, S, σ\},\; (\varphi : MvPolynomial\; σ\; R \to \cdot S)\; (p : MvPolynomial\; σ\; R),\; \varphi p = MvPolynomial.eval_2 (\varphi \circ MvPolynomial.C) (\lambda s, \varphi (MvPolynomial.X s)) p$$$
Lean4
/-- Auxiliary lemma:
Multivariate polynomials in finitely many variables over an integral domain form an integral domain.
This fact is proven by transport of structure from the `MvPolynomial.noZeroDivisors_fin`,
and then used to prove the general case without finiteness hypotheses.
See `MvPolynomial.noZeroDivisors` for the general case. -/
@[deprecated "MvPolynomial.noZeroDivisors" (since := "2025-07-18")]
theorem noZeroDivisors_of_finite (R : Type u) (σ : Type v) [CommSemiring R] [NoZeroDivisors R] :
NoZeroDivisors (MvPolynomial σ R) :=
inferInstance
