isNoetherianRing_of_ringEquiv — Mathlib

English

If R ≃+* S is a ring equivalence and R is Noetherian, then S is Noetherian.

Русский

Если существует эквивалентность колец R и S, и R Ноетеровo, то S Ноетерно.

LaTeX

$$$IsNoetherianRing(S)$ for RingEquiv R S$$

Lean4

theorem isNoetherianRing_of_ringEquiv (R) [Semiring R] {S} [Semiring S] (f : R ≃+* S) [IsNoetherianRing R] :
    IsNoetherianRing S :=
  isNoetherianRing_of_surjective R S f.toRingHom f.toEquiv.surjective

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