Theorems · Theorem · commutative algebra

IsIntegralClosure.of_algEquiv

∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [inst_6 : CommRing S]
  [inst_7 : Algebra A S] [inst_8 : Algebra R S] (f : B ≃ₐ[R] S),
  (∀ (x : A), (algebraMap A S) x = f ((algebraMap A B) x)) → IsIntegralClosure A R S

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebraIsIntegralClosureCommRingAlgebraAlgebra