Theorems · Definition · commutative algebra

Localization.localRingEquiv

{R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} →
      [inst_1 : CommSemiring P] →
        (I : Ideal R) →
          [hI : I.IsPrime] →
            (J : Ideal P) →
              [inst_2 : J.IsPrime] →
                (f : R ≃+* P) → I = Ideal.comap f J → Localization.AtPrime I ≃+* Localization.AtPrime J

Isomorphic rings have isomorphic localizations.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringIdeal.IsPrimeIdeal.IsPrime