Theorems · Definition · commutative algebra

Ideal.quotientEquiv

{R : Type u} →
  [inst : Ring R] →
    {S : Type v} →
      [inst_1 : Ring S] →
        (I : Ideal R) →
          (J : Ideal S) →
            [inst_2 : I.IsTwoSided] → [inst_3 : J.IsTwoSided] → (f : R ≃+* S) → J = Ideal.map (↑f) I → R ⧸ I ≃+* S ⧸ J

The ring equiv R/I ≃+* S/J induced by a ring equiv f : R ≃+* S, where J = f(I).

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingRingIdeal.IsTwoSidedIdeal.IsTwoSided