English
Let R be a commutative ring, S a submonoid of R, P a localization of R, and x ∈ P integral over R. Then the fractional ideal adjoinIntegral(S, x, hx) is exactly the R[x]–fractional ideal of P; i.e., it is the submodule of P generated by all powers of x with coefficients in R.
Русский
Пусть R — коммутативное кольцо, S — подмономиод R, P — локализация R, и элемент x ∈ P интегрирован над R. Тогда соответствующая дробная идея adjoinIntegral(S, x, hx) есть дробная идея R[x] в P; то есть это подмодуля P, порожденного всеми степенями x с коэффициентами в R.
LaTeX
$$$ \\operatorname{adjoinIntegral}(S, x, h_x) = R[x] $$$
Lean4
/-- `FractionalIdeal.adjoinIntegral (S : Submonoid R) x hx` is `R[x]` as a fractional ideal,
where `hx` is a proof that `x : P` is integral over `R`. -/
-- Porting note: `@[simps]` generated a `Subtype.val` coercion instead of a
-- `FractionalIdeal.coeToSubmodule` coercion
def adjoinIntegral (hx : IsIntegral R x) : FractionalIdeal S P :=
⟨_, isFractional_adjoin_integral S x hx⟩
