isNoetherianRing_of_surjective — Mathlib

English

If f: R →+* S is surjective and R is Noetherian, then S is Noetherian.

Русский

Если сюръективен кольцевой гомоморфизм f: R →+* S и R Ноетерово, то S тоже Ноетерово.

LaTeX

$$$IsNoetherianRing(R) \Rightarrow IsNoetherianRing(S)$ for surjective f$$

Lean4

theorem isNoetherianRing_of_surjective (R) [Semiring R] (S) [Semiring S] (f : R →+* S) (hf : Function.Surjective f)
    [H : IsNoetherianRing R] : IsNoetherianRing S :=
  isNoetherian_mk ⟨OrderEmbedding.wellFounded (Ideal.orderEmbeddingOfSurjective f hf).dual H.wf⟩

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