isRegular_prod_X — Mathlib

English

The product of a finite family of variables X_n is a regular element (non-zero divisor) in the multivariate polynomial ring.

Русский

Произведение конечного множества переменных X_n является регулярным элементом (не делителем нуля) в кольце многочленов.

LaTeX

$$$\\prod_{n \\in s} X n$ is regular in the polynomial ring$$

Lean4

@[simp]
theorem isRegular_prod_X (s : Finset σ) : IsRegular (∏ n ∈ s, X n : MvPolynomial σ R) :=
  IsRegular.prod fun _ _ ↦ isRegular_X

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