Theorems · Definition · commutative algebra

RingHom.kerLift

{R : Type u} → {S : Type v} → [inst : Ring R] → [inst_1 : Semiring S] → (f : R →+* S) → R ⧸ RingHom.ker f →+* S

The induced map from the quotient by the kernel to the codomain. This is an isomorphism if f has a right inverse (quotientKerEquivOfRightInverse) / is surjective (quotientKerEquivOfSurjective).

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

13 results in Mathlib

Foundations

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

Assumes

RingSemiring