instIsIntegrallyClosed — Mathlib

English

In a UFD A, A is integrally closed in its fraction field; the instance is provided by the integer_result of integrality.

Русский

В UFD A A интегрально замкнуто в своём поле дробей; инстанс задаётся результатом интегральности.

LaTeX

$$IsIntegrallyClosed A$$

Lean4

instance (priority := 100) instIsIntegrallyClosed : IsIntegrallyClosed A :=
  (isIntegrallyClosed_iff (FractionRing A)).mpr fun {_} => integer_of_integral

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