isNoetherian — Mathlib

English

A variant of the previous statement for a differently indexed ring extension.

Русский

Вариант предыдущего утверждения для другого индексируемого расширения кольца.

LaTeX

$$IsNoetherian R₁ (Subtype fun x => SetLike.instMembership.mem I.coeToSubmodule x)$$

Lean4

/-- Every fractional ideal of a Noetherian integral domain is Noetherian. -/
theorem isNoetherian [IsNoetherianRing R₁] (I : FractionalIdeal R₁⁰ K) : IsNoetherian R₁ I :=
  by
  obtain ⟨d, J, _, rfl⟩ := exists_eq_spanSingleton_mul I
  apply isNoetherian_spanSingleton_inv_to_map_mul
  apply isNoetherian_coeIdeal

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