isIntegrallyClosed_iff_isIntegralClosure

English

Algebra isomorphisms preserve integrally closed property: for e: A ≃ₐ[R] B, IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B.

Русский

Алгебраические изоморфизмы сохраняют интегральную замкнутость: для e:A ≃ₐ[R] B верно IsIntegrallyClosedIn R A ⇔ IsIntegrallyClosedIn R B.

LaTeX

$$$IsIntegrallyClosedIn\,R\,A \iff IsIntegrallyClosedIn\,R\,B$$$

Lean4

/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
theorem isIntegrallyClosed_iff_isIntegralClosure : IsIntegrallyClosed R ↔ IsIntegralClosure R R K :=
  isIntegrallyClosed_iff_isIntegrallyClosedIn K

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