Theorems · Definition · commutative algebra

RingCon.quotientKerEquivOfRightInverse

{M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring P] →
        (f : M →+* P) → (g : P → M) → Function.RightInverse g ⇑f → (RingCon.ker f).Quotient ≃+* P

The first isomorphism theorem for semirings in the case of a homomorphism with right inverse.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

1 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring