English
Let R be a commutative semiring, A and B be commutative rings with R-algebra structures, and f: A →ₐ[R] B an R-algebra hom. If A is Noetherian, then the image of A in B is a Noetherian ring.
Русский
Пусть R — коммутативное полукольцо, A и B — коммутативные кольца с структурами R-алгебр, и f: A →ₐ[R] B — алгебра-гомоморфизм над R. Если A является кольцом Неттерa, то образ f(A) внутри B является кольцом Неттерa.
LaTeX
$$$\\operatorname{IsNoetherianRing}(\\operatorname{Im}(f))$$$
Lean4
/-- The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring. -/
instance isNoetherianRing_range (f : A →ₐ[R] B) [IsNoetherianRing A] : IsNoetherianRing f.range :=
_root_.isNoetherianRing_range f.toRingHom
