isNoetherian_of_liesOver — Mathlib

English

Let A and B be rings with B a Noetherian A-module and p ⊆ A, P ⊆ B ideals such that P lies over p. Then B/P is a Noetherian module over A/p.

Русский

Пусть A и B — кольца, B является Noetherian A-модулем, и P ⊆ B, p ⊆ A — идеалы, причём P лежит над p. Тогда B/P является Noetherian A/p-модулем.

LaTeX

$$$IsNoetherian(A/ p)\,(B/ P)$$$

Lean4

/-- `B ⧸ P` is a Noetherian `A ⧸ p`-module if `B` is a Noetherian `A`-module. -/
instance isNoetherian_of_liesOver [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ P) :=
  isNoetherian_of_tower A inferInstance

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