isNoetherianRing — Mathlib

English

If R is Noetherian, then the multivariate polynomial ring in Finite n variables is Noetherian.

Русский

Если R является Нётеровым кольцом, то многочлены в Finite n переменных образуют Нётерово кольцо.

LaTeX

$$$\forall n : \mathbb{N},\; \operatorname{IsNoetherianRing}(\mathrm{MvPolynomial}(\mathrm{Fin}(n), R))$$$

Lean4

/-- The multivariate polynomial ring in finitely many variables over a Noetherian ring
is itself a Noetherian ring. -/
instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R) :=
  by
  cases nonempty_fintype σ
  exact
    @isNoetherianRing_of_ringEquiv (MvPolynomial (Fin (Fintype.card σ)) R) _ _ _
      (renameEquiv R (Fintype.equivFin σ).symm).toRingEquiv isNoetherianRing_fin

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