Theorems · Theorem · commutative algebra

RingHom.quotientKerEquivOfRightInverse.apply

∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {g : S → R}
  (hf : Function.RightInverse g ⇑f) (x : R ⧸ RingHom.ker f), (RingHom.quotientKerEquivOfRightInverse hf) x = f.kerLift x

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingSemiring