extension_isNoetherian — Mathlib

English

K is the localization of 𝓞_K by the nonzero integers: 𝓞_K[(ℤ\\{0})^{-1}] ≅ K.

Русский

K — локализация 𝓞_K по не нулевым целым: 𝓞_K[(ℤ\\{0})^{-1}] ≅ K.

LaTeX

$$IsLocalization(Algebra.algebraMapSubmonoid(𝓞_K)(nonZeroDivisors ℤ)) K$$

Lean4

/-- Any extension between ring of integers of number fields is Noetherian. -/
instance extension_isNoetherian [NumberField K] [NumberField L] : IsNoetherian (𝓞 K) (𝓞 L) :=
  IsIntegralClosure.isNoetherian (𝓞 K) K L (𝓞 L)

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