Theorems · Theorem · commutative algebra

Ideal.map_mk_comap_factor

∀ {R : Type u_1} [inst : Ring R] {I J K : Ideal R} [inst_1 : J.IsTwoSided] [inst_2 : K.IsTwoSided],
  J ≤ I →
    ∀ (hJK : K ≤ J),
      Ideal.comap (Ideal.Quotient.factor hJK) (Ideal.map (Ideal.Quotient.mk J) I) = Ideal.map (Ideal.Quotient.mk K) I

Defined in

Mathlib.RingTheory.Ideal.Quotient.PowTransition

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSidedIdeal.IsTwoSided