isNoetherianRing — Mathlib

English

If IsDedekindDomainInv A holds for a domain A, then A is Noetherian.

Русский

Если для домена A выполняется IsDedekindDomainInv, тогда A является Noetherian.

LaTeX

$$$$\\text{IsDedekindDomainInv}(A) \\Rightarrow \\text{IsNoetherianRing}(A).$$$$

Lean4

theorem isNoetherianRing : IsNoetherianRing A :=
  by
  refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩
  by_cases hI : I = ⊥
  · rw [hI]; apply Submodule.fg_bot
  have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
  exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) (h.isUnit hI)

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