instIsReduced — Mathlib

English

If R is a reduced ring, then the multivariate polynomial ring MvPolynomial σ R is reduced.

Русский

Пусть R — редуцированное кольцо. Тогда кольцо многочленов MvPolynomial σ R редуировано.

LaTeX

$$$$ \\operatorname{IsReduced}(R) \\Rightarrow \\operatorname{IsReduced}(\\operatorname{MvPolynomial}_{\\sigma} R). $$$$

Lean4

instance [IsReduced R] : IsReduced (MvPolynomial σ R) := by simp [isReduced_iff, isNilpotent_iff, MvPolynomial.ext_iff]

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