isIntegral_iff — Mathlib

English

Let e: A ≃ₐ[R] B be an R-algebra isomorphism. Then A is integral over R if and only if B is integral over R.

Русский

Пусть e: A ≃ₐ[R] B — изоморфизм R-алгебр. Тогда A интегральна над R тогда и только тогда, когда B интегральна над R.

LaTeX

$$$(\exists e: A \simeq_R B)\; (\text{Algebra.IsIntegral } R\ A) \iff (\text{Algebra.IsIntegral } R\ B).$$$

Lean4

theorem isIntegral_iff (e : A ≃ₐ[R] B) : Algebra.IsIntegral R A ↔ Algebra.IsIntegral R B :=
  ⟨fun h ↦ h.of_injective e.symm e.symm.injective, fun h ↦ h.of_injective e e.injective⟩

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