isNoetherianRing_fin_0 — Mathlib

English

If R is a Noetherian ring, then the multivariate polynomial ring in zero variables over R is Noetherian.

Русский

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

LaTeX

$$$\operatorname{IsNoetherianRing} (\mathrm{MvPolynomial}(\mathrm{Fin}(0), R))$$$

Lean4

theorem isNoetherianRing_fin_0 [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial (Fin 0) R) :=
  by
  apply isNoetherianRing_of_ringEquiv R
  symm; apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

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