instFiniteSubtypeMemIdealOfIsNoetherian

English

If R₁ is a commutative semiring, S is a semiring with a Noetherian R₁-algebra structure, and I is an ideal of S, then the subtype of I (as an R₁-module) is finite.

Русский

Пусть R₁ — коммутативный полупрямой; S — полупрямой, имеющий структуру алгебры над R₁; I — идеал S; тогда подмножество I как R₁-модуль конечно.

LaTeX

$$$[CommSemiring R_1] [Semiring S] [Algebra R_1 S] [IsNoetherian R_1 S](I: \text{Ideal } S)\Rightarrow Module.Finite R_1 (Subtype fun x => x \in I)$$$

Lean4

instance {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [IsNoetherian R₁ S] (I : Ideal S) :
    Module.Finite R₁ I :=
  IsNoetherian.finite R₁ ((I : Submodule S S).restrictScalars R₁)

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