English
In a Noetherian ring R, the multivariate polynomial ring in Finite n variables has no zero divisors when R is an integral domain (NoZeroDivisors).
Русский
В кольце с нулевыми делителями отсутствуют нулевые делители в многочленовом кольце Finite n переменных над интегральным доменом.
LaTeX
$$$\operatorname{NoZeroDivisors}(\mathrm{MvPolynomial}(\mathrm{Fin}(n), R))$$$
Lean4
/-- Auxiliary lemma:
Multivariate polynomials over an integral domain
with variables indexed by `Fin n` form an integral domain.
This fact is proven inductively,
and then used to prove the general case without any finiteness hypotheses.
See `MvPolynomial.noZeroDivisors` for the general case. -/
@[deprecated "MvPolynomial.noZeroDivisors" (since := "2025-07-18")]
theorem noZeroDivisors_fin (R : Type u) [CommSemiring R] [NoZeroDivisors R] :
∀ n : ℕ, NoZeroDivisors (MvPolynomial (Fin n) R) := fun _ ↦ inferInstance
