isNoetherianRing_fin — Mathlib

English

For any natural number n, the multivariate polynomial ring in Finite n variables over a Noetherian ring R is Noetherian.

Русский

Для любого конечного числа n многочленовый кольцо в n переменных над кольцом R, являющимся Нётеровым, также является Нётеровым.

LaTeX

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

Lean4

theorem isNoetherianRing_fin [IsNoetherianRing R] : ∀ {n : ℕ}, IsNoetherianRing (MvPolynomial (Fin n) R)
  | 0 => isNoetherianRing_fin_0
  | n + 1 =>
    @isNoetherianRing_of_ringEquiv (Polynomial (MvPolynomial (Fin n) R)) _ _ _
      (MvPolynomial.finSuccEquiv _ n).toRingEquiv.symm
      (@Polynomial.isNoetherianRing (MvPolynomial (Fin n) R) _ isNoetherianRing_fin)

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