finite_adjoin_simple_of_isIntegral

English

If x is integral over R, then the R-submodule underlying the adjoin R {x} is finitely generated.

Русский

Если x интегральен над R, то подмодуль над R, порожденный adjoin R {x}, порожден конечным числом элементов.

LaTeX

$$$\\operatorname{Module.Finite}_R\\bigl(\\mathrm{adjoin}\\ R\\{x\\}\\bigr)$$$

Lean4

theorem finite_adjoin_simple_of_isIntegral {x : B} (hi : IsIntegral R x) : Module.Finite R (adjoin R { x }) :=
  Module.Finite.iff_fg.mpr hi.fg_adjoin_singleton

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