Theorems · Theorem · commutative algebra

Ideal.ker_quotient_lift

∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {I : Ideal R} [inst_2 : I.IsTwoSided] (f : R →+* S)
  (H : I ≤ RingHom.ker f), RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

4 results in Mathlib

Foundations

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

Assumes

RingSemiringIdeal.IsTwoSided