isFractional_adjoin_integral — Mathlib

English

If x is integral over R, then the submodule generated by x inside the algebra adjoin is fractional over S.

Русский

Если x интегрален над R, то подмодуль порожденный x внутри адъоянации является дробным над S.

LaTeX

$$IsIntegral R x → IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R { x }))$$

Lean4

/-- `A[x]` is a fractional ideal for every integral `x`. -/
theorem isFractional_adjoin_integral (hx : IsIntegral R x) :
    IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R ({ x } : Set P))) :=
  isFractional_of_fg hx.fg_adjoin_singleton

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