isIntegrallyClosedIn — Mathlib

English

Being integrally closed is preserved under algebra isomorphisms: if e: A ≃ₐ[R] B, then IsIntegrallyClosedIn R A holds iff IsIntegrallyClosedIn R B holds.

Русский

Интегральная замкнутость сохраняется при алгебраических изоморфизмах: если e:A ≃ₐ[R] B, то IsIntegrallyClosedIn R A эквивалентно IsIntegrallyClosedIn R B.

LaTeX

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

Lean4

/-- Being integrally closed is preserved under algebra isomorphisms. -/
theorem isIntegrallyClosedIn (e : A ≃ₐ[R] B) : IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B :=
  ⟨AlgHom.isIntegrallyClosedIn e.symm e.symm.injective, AlgHom.isIntegrallyClosedIn e e.injective⟩

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