feat(RingTheory/IntegralClosure/IsIntegralClosure/Basic): add isInteg…

…ral_iff_of_equiv (#15738)

Co-authored-by: Filippo A. E. Nuccio <[email protected]>

Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

@@ -185,3 +185,7 @@ def integralClosure : Subalgebra R A where
   algebraMap_mem' _ := isIntegral_algebraMap
 
 end
+
+theorem mem_integralClosure_iff (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] {a : A} :
+    a ∈ integralClosure R A ↔ IsIntegral R a :=
+  Iff.rfl

Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

@@ -131,6 +131,26 @@ theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B}
   let ⟨p, hp, hpx⟩ := hx
   ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩
 
+/- If `R` and `T` are isomorphic commutative rings and `S` is an `R`-algebra and a `T`-algebra in
+  a compatible way, then an element `a ∈ S` is integral over `R` if and only if it is integral
+  over `T`.-/
+theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
+    [Algebra R S] [Algebra T S] (φ : R ≃+* T)
+    (h : (algebraMap T S).comp φ.toRingHom = algebraMap R S) (a : S) :
+    IsIntegral R a ↔ IsIntegral T a := by
+  constructor <;> intro ha
+  · letI : Algebra R T := φ.toRingHom.toAlgebra
+    letI : IsScalarTower R T S :=
+      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
+    exact IsIntegral.tower_top ha
+  · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
+      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm,
+        RingHomCompTriple.comp_eq]
+    letI : Algebra T R := φ.symm.toRingHom.toAlgebra
+    letI : IsScalarTower T R S :=
+      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
+    exact IsIntegral.tower_top ha
+
 theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B}
     [FunLike F B C] [RingHomClass F B C] (f : F)
     (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) :=