mem_adjoinIntegral_self — Mathlib

English

If hx : IsIntegral R x, then x ∈ adjoinIntegral S x hx; i.e., x lies in the fractional ideal generated by x over R.

Русский

Пусть hx: IsIntegral R x. Тогда x ∈ adjoinIntegral(S, x, hx); то есть x принадлежит дробной идее, порождаемой x над R.

LaTeX

$$$ x \\in \\operatorname{adjoinIntegral}(S, x, h_x) $$$

Lean4

theorem mem_adjoinIntegral_self (hx : IsIntegral R x) : x ∈ adjoinIntegral S x hx :=
  Algebra.subset_adjoin (Set.mem_singleton x)

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