fg_of_isNoetherianRing — Mathlib

English

If R is Noetherian, then fractional ideals over R are finitely generated.

Русский

Если R — кольцо Ноетеринa, дробные идеалы над R являются конечно порожденными.

LaTeX

$$$\text{The fractional ideals of a Noetherian ring are finitely generated}$$$

Lean4

/-- The fractional ideals of a Noetherian ring are finitely generated. -/
theorem fg_of_isNoetherianRing [hR : IsNoetherianRing R] (hS : S ≤ R⁰) (I : FractionalIdeal S P) :
    FG I.coeToSubmodule := by
  have := hR.noetherian I.num
  rw [← fg_top] at this ⊢
  exact fg_of_linearEquiv (I.equivNum <| coe_ne_zero ⟨(I.den : R), hS (SetLike.coe_mem I.den)⟩) this

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