integer_of_integral — Mathlib

English

In a UFD A, A is integrally closed in its fraction field; equivalently, every element integral over A already lies in A.

Русский

В UFD A кольцо A интегрально замкнуто в своём поле дробей: каждый элемент, интегральный над A, уже лежит в A.

LaTeX

$$IsIntegrallyClosed A$$

Lean4

theorem integer_of_integral {x : K} : IsIntegral A x → IsInteger A x := fun ⟨_, hp, hx⟩ =>
  isInteger_of_is_root_of_monic hp hx

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