Theorems · Definition · commutative algebra

Ideal.Quotient.lift

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

Given a ring homomorphism f : R →+* S sending all elements of an ideal to zero, lift it to the quotient by this ideal.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Defs

Cited by

19 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSidedSemiring