English
For hx : IsIntegral R x, the underlying Submodule of adjoinIntegral S x hx coincides with the Subalgebra-generated submodule; namely, (adjoinIntegral S x hx : Submodule R P) = Subalgebra.toSubmodule(Algebra.adjoin R { x }).
Русский
Пусть hx: IsIntegral R x. Тогда приводимая к подмодулю часть adjoinIntegral(S, x, hx) совпадает с подмодулем, порождаемым подалгеброй; то есть (adjoinIntegral S x hx : Submodule R P) = Subalgebra.toSubmodule(Algebra.adjoin R { x }).
LaTeX
$$$ (\\operatorname{adjoinIntegral}(S, x, h_x) : \\mathrm{Submodule}\\, R\\, P) = \\mathrm{Subalgebra.toSubmodule}(\\mathrm{Algebra.adjoin}\\, R \\{ x \\}) $$$
Lean4
@[simp]
theorem adjoinIntegral_coe (hx : IsIntegral R x) :
(adjoinIntegral S x hx : Submodule R P) = (Subalgebra.toSubmodule (Algebra.adjoin R ({ x } : Set P))) :=
rfl
