Theorems · Theorem · commutative algebra

Ideal.injective_lift_iff

∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {I : Ideal R} [inst_2 : I.IsTwoSided] {f : R →+* S}
  (H : ∀ a ∈ I, f a = 0), Function.Injective ⇑(Ideal.Quotient.lift I f H) ↔ RingHom.ker f = I

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingSemiringIdeal.IsTwoSided