Theorems · Theorem · commutative algebra

Ideal.Quotient.lift_surjective_of_surjective

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

Defined in

Mathlib.RingTheory.Ideal.Quotient.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSidedSemiring